aboutsummaryrefslogtreecommitdiff
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml5
1 files changed, 3 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8b79dbf810..2581b25715 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -69,6 +69,7 @@ before_script:
- _install_ci
- config/Makefile
- config/coq_config.py
+ - config/coq_config.ml
- test-suite/misc/universes/all_stdlib.v
expire_in: 1 week
script:
@@ -172,7 +173,7 @@ before_script:
- BIN=$(readlink -f ../_install_ci/bin)/
- LIB=$(readlink -f ../_install_ci/lib/coq)/
- export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
- - make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all
+ - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" all
artifacts:
name: "$CI_JOB_NAME.logs"
when: on_failure
@@ -531,7 +532,7 @@ test-suite:base+async:
needs:
- build:base
variables:
- COQFLAGS: "-async-proofs on -async-proofs-cache force"
+ COQEXTRAFLAGS: "-async-proofs on -async-proofs-cache force"
timeout: 100m
allow_failure: true
only: