Handle PR not found in post-merge workflow

Author: Kobzol

.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 <[email protected]>' -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