diff options
| -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 |