diff options
| author | Emilio Jesus Gallego Arias | 2019-02-18 19:37:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-18 19:37:41 +0100 |
| commit | 69f219cdcddc10823d52ffa1ea9503254e48bce4 (patch) | |
| tree | fa3ad49134db01a4c0c074ade4fc7c17584689b2 | |
| parent | fcc3ee5d3eed4703e88fc1a2f07006130b61d006 (diff) | |
| parent | 1dd6403786831ba4017ffef2d6f0090d53b3a2f6 (diff) | |
Merge PR #9600: CI: fix trunk jobs switch picking
Reviewed-by: ejgallego
| -rw-r--r-- | .gitlab-ci.yml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f5a5d6d45a..f8278fa1f5 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -436,7 +436,7 @@ test-suite:edge+trunk+make: - make -j "$NJOBS" world - make -j "$NJOBS" test-suite UNIT_TESTS= variables: - OPAM_SWITCH: edge + OPAM_SWITCH: base artifacts: name: "$CI_JOB_NAME.logs" when: always @@ -462,7 +462,7 @@ test-suite:edge+trunk+dune: - export COQ_UNIT_TEST=noop - dune runtest --profile=ocaml409 variables: - OPAM_SWITCH: edge + OPAM_SWITCH: base artifacts: name: "$CI_JOB_NAME.logs" when: always |