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 /src/ci/github-actions | |
| parent | 71384101ea3b030b80f7def80a37f67e148518b0 (diff) | |
| download | rust-5e11ae4fc52e749f43d334e96ba06c979fa67ef7.tar.gz rust-5e11ae4fc52e749f43d334e96ba06c979fa67ef7.zip | |
ci: allow RLA to pick the right PR number
Diffstat (limited to 'src/ci/github-actions')
| -rw-r--r-- | src/ci/github-actions/ci.yml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/ci/github-actions/ci.yml b/src/ci/github-actions/ci.yml index 5573d87aa2e..d2b804f08c3 100644 --- a/src/ci/github-actions/ci.yml +++ b/src/ci/github-actions/ci.yml @@ -92,6 +92,15 @@ x--expand-yaml-anchors--remove: if: success() && !env.SKIP_JOB && github.ref != 'refs/heads/try' <<: *step + # Rust Log Analyzer can't currently detect the PR number of a GitHub + # Actions build on its own, so a hint in the log message is needed to + # point it in the right direction. + - 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: |