We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
2 parents 74e5184 + a84a946 commit ee0d68fCopy full SHA for ee0d68f
.github/workflows/post-merge.yml
@@ -25,12 +25,19 @@ jobs:
25
env:
26
GH_TOKEN: ${{ github.token }}
27
run: |
28
+ # Give GitHub some time to propagate the information that the PR was merged
29
+ sleep 60
30
+
31
# Get closest bors merge commit
32
PARENT_COMMIT=`git rev-list --author='bors <[email protected]>' -n1 --first-parent HEAD^1`
33
echo "Parent: ${PARENT_COMMIT}"
34
35
# Find PR for the current commit
36
HEAD_PR=`gh pr list --search "${{ github.sha }}" --state merged --json number --jq '.[0].number'`
37
+ if [ -z "${HEAD_PR}" ]; then
38
+ echo "PR for commit SHA ${{ github.sha }} not found, exiting"
39
+ exit 1
40
+ fi
41
echo "HEAD: ${{ github.sha }} (#${HEAD_PR})"
42
43
cd src/ci/citool
0 commit comments