chore: pr-release.yml: use API to get pull request number (#3066)

partially reverting 6a629f7. What a mess.
leanprover · Dec 13, 2023 · df18f3f · df18f3f
1 parent fbcfe65
commit df18f3f
Showing 1 changed file with 18 additions and 5 deletions.
diff --git 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