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