Skip to content

Commit

Permalink
chore: robustify PR release workflow (#3051)
Browse files Browse the repository at this point in the history
the workflow is triggered not only by pull-request-CI-runs but also by
others. These should be skipped.

Also, no need to query the Github API to get the pull request number and
head sha, they are part of the payload, it seems.
  • Loading branch information
nomeata authored Dec 12, 2023
1 parent f74516a commit 6a629f7
Showing 1 changed file with 5 additions and 9 deletions.
14 changes: 5 additions & 9 deletions .github/workflows/pr-release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,16 @@ on:
jobs:
on-success:
runs-on: ubuntu-latest
if: github.event.workflow_run.conclusion == 'success' && github.repository == 'leanprover/lean4'
if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
steps:
- name: Retrieve PR number and head commit
- name: Set PR number and head commit
uses: actions/github-script@v7
id: workflow-info
with:
script: |
const reply = await github.rest.actions.getWorkflowRun({
owner: context.repo.owner,
repo: context.repo.repo,
run_id: context.payload.workflow_run.id,
})
core.setOutput('pullRequestNumber', reply.data.pull_requests[0].number)
core.setOutput('sourceHeadSha', reply.data.pull_requests[0].head.sha)
// 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)
- name: Download artifact from the previous workflow.
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
Expand Down

0 comments on commit 6a629f7

Please sign in to comment.