updated gb quickstart #72
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Auto Merge PR branches to Devel | |
| on: | |
| pull_request: | |
| branches: | |
| - main | |
| types: | |
| - opened | |
| - synchronize | |
| - reopened | |
| jobs: | |
| merge-to-devel: | |
| # This condition checks if the PR has the "automerge" label | |
| if: contains(github.event.pull_request.labels.*.name, 'automerge') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v2 | |
| with: | |
| fetch-depth: 0 | |
| - name: Set Git User | |
| run: | | |
| git config --global user.email "github-actions[bot]@users.noreply.github.com" | |
| git config --global user.name "GitHub Actions Bot" | |
| - name: Merge to Devel | |
| run: | | |
| git checkout devel | |
| git merge --no-ff --no-commit origin/${{ github.head_ref }} | |
| git commit -m "Merged ${{ github.head_ref }} into devel (from PR)" | |
| git push origin devel |