Skip to content

Commit

Permalink
chore: refactor pr-release.yml to avoid 'await' (#3070)
Browse files Browse the repository at this point in the history
#3066 is causing CI failures, e.g.
[here](https://github.com/leanprover/lean4/actions/runs/7202184616/job/19619827364).

Although there are plenty of examples of using `await` in a Github
workflow script block, the error *seems* to be about this. This refactor
hopefully works around that, but I'm still uncertain of a root cause.
  • Loading branch information
kim-em authored Dec 14, 2023
1 parent df18f3f commit f208d7b
Showing 1 changed file with 18 additions and 13 deletions.
31 changes: 18 additions & 13 deletions .github/workflows/pr-release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,23 +23,28 @@ jobs:
id: workflow-info
with:
script: |
# 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({
const run_id = context.payload.workflow_run.id;
console.log(`Querying workflow run data for run_id ${run_id}.`);
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")
}
.then(reply => {
if (reply.data.pull_requests && reply.data.pull_requests.length > 0) {
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");
}
})
.catch(error => {
console.error(error);
core.setFailed("Error querying workflow run data: " + error.message);
});
- name: Download artifact from the previous workflow.
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
id: download-artifact
Expand Down

0 comments on commit f208d7b

Please sign in to comment.