diff options
| author | Gaëtan Gilbert | 2020-09-21 14:25:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-09-21 14:25:39 +0200 |
| commit | 14aaac29871328d6a369d52d8febd74afc727d64 (patch) | |
| tree | 8dc926d4b79b79c311e9fad8fd49a9b489ecb712 /.gitlab-ci.yml | |
| parent | fff4fe1120c81ab7b543cfb8d175cc4458e3c12e (diff) | |
fix build:quick and build:base+async artifacts
We put dmesg.txt in the artifact path for all build-template users,
but only these 2 jobs produce it to avoid uploading unused data (see
discussion in #13043).
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7d22be71a1..116d895600 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -79,6 +79,7 @@ before_script: - config/coq_config.py - config/coq_config.ml - test-suite/misc/universes/all_stdlib.v + - dmesg.txt expire_in: 1 week script: - set -e @@ -338,10 +339,7 @@ build:base+async: variables: - $UNRELIABLE =~ /enabled/ artifacts: - name: "$CI_JOB_NAME" - when: on_failure - paths: - - dmesg.txt + when: always build:quick: extends: .build-template @@ -356,10 +354,7 @@ build:quick: variables: - $UNRELIABLE =~ /enabled/ artifacts: - name: "$CI_JOB_NAME" - when: on_failure - paths: - - dmesg.txt + when: always windows64: extends: .windows-template |