From 6a629f7d7ff20684102a6d6a106b265aea74f4db Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 12 Dec 2023 12:23:22 +0100 Subject: [PATCH] chore: robustify PR release workflow (#3051) 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. --- .github/workflows/pr-release.yml | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 943914ac9f6e..6821c4aa711d 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -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 != '' }}