Handle PR not found in post-merge workflow

This commit is contained in:
Jakub Beránek 2025-05-06 16:10:58 +02:00
parent f5d3fe273b
commit a84a946a3d
No known key found for this signature in database
GPG Key ID: 909CD0D26483516B

View File

@ -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