max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

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

Browse source 
partially reverting 6a629f7d7f. What a
mess.
This commit is contained in:
Joachim Breitner 2023-12-13 20:58:14 +01:00 • committed by GitHub
parent fbcfe6596e
commit df18f3f1ff
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 18 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
.github/workflows/pr-release.yml vendored
View file

@ -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