From df18f3f1ff1f46ae970c7eff0e9d2a97e83619d1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 13 Dec 2023 20:58:14 +0100
Subject: [PATCH] chore: pr-release.yml: use API to get pull request number
 (#3066)

partially reverting 6a629f7d7ff20684102a6d6a106b265aea74f4db. What a
mess.
---
 .github/workflows/pr-release.yml | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
index d0598e6aff..8ec6cecd0c 100644
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -18,15 +18,28 @@ jobs:
     runs-on: ubuntu-latest
     if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
     steps:
-      - name: Set PR number and head commit
+      - name: Retrieve PR number and head commit
         uses: actions/github-script@v7
         id: workflow-info
         with:
           script: |
-            console.log(`context.payload: ${JSON.stringify(context.payload, null, 2)}`)
-            core.setOutput('pullRequestNumber', context.payload.workflow_run.pull_requests[0].number)
-            core.setOutput('sourceHeadSha',     context.payload.workflow_run.pull_requests[0].head.sha)
-
+            # strangely, the array context.payload.workflow_run.pull_requests is
+            # sometimes empty. So get the data via tha API
+            const run_id = context.payload.workflow_run.id
+            console.log(`Querying workflow run data for run_id ${run_id}.`)
+            const reply = await github.rest.actions.getWorkflowRun({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                run_id: run_id
+            })
+            if (reply.data.pull_requests) {
+              core.setOutput('pullRequestNumber', reply.data.pull_requests[0].number)
+              core.setOutput('sourceHeadSha',     reply.data.pull_requests[0].head.sha)
+            } else {
+              console.log("Odd, no pull-request-data in workflow data?")
+              console.log(`reply.data: ${JSON.stringify(reply.data, null, 2)}`)
+              core.setFailed("Unexpected result from github.rest.actions.getWorkflowRun")
+            }
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact