diff options
| author | Enrico Tassi | 2020-03-20 14:26:48 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-03-20 14:26:48 +0100 |
| commit | 5b7a6471cf812a708dbbb8943f30d525e46250f6 (patch) | |
| tree | caf236823940843f1609112162801250bf5dfdb6 /.gitlab-ci.yml | |
| parent | 06b820259989a59080d0dc68bf0c633994fe221f (diff) | |
| parent | 57bc1b7921da4ae54ee5d3b999351f297556fd65 (diff) | |
Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yes
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 621374da0e..4a053ec03f 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: |