diff options
| author | Pietro Albini <pietro@pietroalbini.org> | 2020-07-20 17:11:30 +0200 |
|---|---|---|
| committer | Pietro Albini <pietro@pietroalbini.org> | 2020-07-20 17:12:30 +0200 |
| commit | 5e11ae4fc52e749f43d334e96ba06c979fa67ef7 (patch) | |
| tree | e71fda9f3e1aca57a5fc7ac60223706d8e644546 /.github/workflows | |
| parent | 71384101ea3b030b80f7def80a37f67e148518b0 (diff) | |
ci: allow RLA to pick the right PR number
Diffstat (limited to '.github/workflows')
| -rw-r--r-- | .github/workflows/ci.yml | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 86de3782000..e3525efd4b6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -63,6 +63,11 @@ jobs: with: github_token: "${{ secrets.github_token }}" if: "success() && !env.SKIP_JOB && github.ref != 'refs/heads/try'" + - name: configure the PR in which the error message will be posted + run: "echo \"[CI_PR_NUMBER=$num]\"" + env: + num: "${{ github.event.number }}" + if: "success() && !env.SKIP_JOBS && github.event_name == 'pull_request'" - name: add extra environment variables run: src/ci/scripts/setup-environment.sh env: @@ -162,6 +167,11 @@ jobs: with: github_token: "${{ secrets.github_token }}" if: "success() && !env.SKIP_JOB && github.ref != 'refs/heads/try'" + - name: configure the PR in which the error message will be posted + run: "echo \"[CI_PR_NUMBER=$num]\"" + env: + num: "${{ github.event.number }}" + if: "success() && !env.SKIP_JOBS && github.event_name == 'pull_request'" - name: add extra environment variables run: src/ci/scripts/setup-environment.sh env: @@ -479,6 +489,11 @@ jobs: with: github_token: "${{ secrets.github_token }}" if: "success() && !env.SKIP_JOB && github.ref != 'refs/heads/try'" + - name: configure the PR in which the error message will be posted + run: "echo \"[CI_PR_NUMBER=$num]\"" + env: + num: "${{ github.event.number }}" + if: "success() && !env.SKIP_JOBS && github.event_name == 'pull_request'" - name: add extra environment variables run: src/ci/scripts/setup-environment.sh env: @@ -604,6 +619,11 @@ jobs: with: github_token: "${{ secrets.github_token }}" if: "success() && !env.SKIP_JOB && github.ref != 'refs/heads/try'" + - name: configure the PR in which the error message will be posted + run: "echo \"[CI_PR_NUMBER=$num]\"" + env: + num: "${{ github.event.number }}" + if: "success() && !env.SKIP_JOBS && github.event_name == 'pull_request'" - name: add extra environment variables run: src/ci/scripts/setup-environment.sh env: |