diff options
| author | Gaëtan Gilbert | 2018-05-14 13:43:55 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-14 13:45:27 +0200 |
| commit | eed834b337354251dfd0ae60c8358f4d126420b2 (patch) | |
| tree | a68b66e9a5f795d971070afdc6948d8709f6ffde | |
| parent | 4094a8c2cac668db112fc84f5d1b287eacbf6700 (diff) | |
gitlab CI: fix [warnings] template
We never actually used the -warn-error flag...
| -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 2f5a000169..496444f7d1 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 @@ -171,6 +171,7 @@ warnings:base: warnings:edge: <<: *warnings-template variables: + <<: *warnings-variables OPAM_SWITCH: edge test-suite:base: |