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 != '' }}