diff options
| author | Jakub Beránek <berykubik@gmail.com> | 2025-05-06 16:10:58 +0200 |
|---|---|---|
| committer | Jakub Beránek <berykubik@gmail.com> | 2025-05-06 18:35:05 +0200 |
| commit | a84a946a3d6fc60f6485cf1d8a47845d3a416117 (patch) | |
| tree | 72df19c9e9909d93a21c184832afb52d44f8bb5a /.github | |
| parent | f5d3fe273b8b9e7125bf8856d44793b6cc4b6735 (diff) | |
| download | rust-a84a946a3d6fc60f6485cf1d8a47845d3a416117.tar.gz rust-a84a946a3d6fc60f6485cf1d8a47845d3a416117.zip | |
Handle PR not found in post-merge workflow
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/post-merge.yml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/.github/workflows/post-merge.yml b/.github/workflows/post-merge.yml index 94553608a2f..ca088ba31fd 100644 --- a/.github/workflows/post-merge.yml +++ b/.github/workflows/post-merge.yml @@ -25,12 +25,19 @@ jobs: env: GH_TOKEN: ${{ github.token }} run: | + # Give GitHub some time to propagate the information that the PR was merged + sleep 60 + # Get closest bors merge commit PARENT_COMMIT=`git rev-list --author='bors <bors@rust-lang.org>' -n1 --first-parent HEAD^1` echo "Parent: ${PARENT_COMMIT}" # Find PR for the current commit HEAD_PR=`gh pr list --search "${{ github.sha }}" --state merged --json number --jq '.[0].number'` + if [ -z "${HEAD_PR}" ]; then + echo "PR for commit SHA ${{ github.sha }} not found, exiting" + exit 1 + fi echo "HEAD: ${{ github.sha }} (#${HEAD_PR})" cd src/ci/citool |