diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 01:38:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 01:38:57 +0200 |
| commit | acdb3608cb1faf18826981ba2fecd8e7781e5e4b (patch) | |
| tree | 207f63b5fb717b1d37cd3eb8ab58a018e44e394a /.gitlab-ci.yml | |
| parent | f2e59e74aeaa8ce9a0317cb87eae99fb0ec14ae3 (diff) | |
| parent | eed834b337354251dfd0ae60c8358f4d126420b2 (diff) | |
Merge PR #7507: gitlab CI: fix [warnings] template
Diffstat (limited to '.gitlab-ci.yml')
| -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: |