diff options
| -rw-r--r-- | .gitlab-ci.yml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 095099690..656fd741f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -76,7 +76,7 @@ before_script: - set +e variables: &warnings-variables - COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" + COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes" # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that @@ -199,6 +199,7 @@ warnings:base: warnings:edge: <<: *warnings-template variables: + <<: *warnings-variables OPAM_SWITCH: edge test-suite:base: |