diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 1d43a8b3bbd4..0965443db590 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -16,7 +16,7 @@ on: jobs: on-success: runs-on: ubuntu-latest - if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4' + if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' steps: - name: Set PR number and head commit uses: actions/github-script@v7