replace dev/script/push-pr.sh with an equivalent GHA via `workflow_…
#3
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: push-pr | |
| on: | |
| push: | |
| branches: | |
| - 'move_push-pr_script_to_GHA' #FIXME remove as temporary to check this workflow works | |
| workflow_dispatch: # | |
| inputs: | |
| prNumber: | |
| description: 'PR number' | |
| required: true | |
| type: string | |
| # we decided not to have 'workflow_run' here (chained of CI success) for 'trusted' forks, as we don't know/control the | |
| # access control etc. - so keeping it manual only (via workflow_dispatch above) | |
| # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run: | |
| jobs: | |
| push: | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: push-pr | |
| env: | |
| PR: ${{ inputs.prNumber || 4212 }} | |
| run: | | |
| echo "Pushing PR merge commit for ${PR} to remote pr${PR} branch" | |
| git fetch -f origin pull/${PR}/merge:pr${PR} | |
| git push -f origin pr${PR}:pr${PR} |