From a84a946a3d6fc60f6485cf1d8a47845d3a416117 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Ber=C3=A1nek?= <berykubik@gmail.com>
Date: Tue, 6 May 2025 16:10:58 +0200
Subject: [PATCH] Handle PR not found in post-merge workflow

---
 .github/workflows/post-merge.yml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.github/workflows/post-merge.yml b/.github/workflows/post-merge.yml
index 94553608a2f48..ca088ba31fdf9 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