diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 12287d4263d4..8f37b9831a80 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -18,33 +18,15 @@ 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: Retrieve PR number and head commit - uses: actions/github-script@v7 + - name: Retrieve information about the original workflow + uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin + # This action is deprecated and archived, but it seems hard to find a better solution for getting the PR number + # see https://github.com/orgs/community/discussions/25220 for some discussion id: workflow-info with: - script: | - 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 - }) - .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); - }); + token: ${{ secrets.GITHUB_TOKEN }} + sourceRunId: ${{ github.event.workflow_run.id }} + - name: Download artifact from the previous workflow. if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} id: download-artifact