From eed834b337354251dfd0ae60c8358f4d126420b2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 14 May 2018 13:43:55 +0200
Subject: gitlab CI: fix [warnings] template

We never actually used the -warn-error flag...
---
 .gitlab-ci.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to '.gitlab-ci.yml')

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2f5a00016..496444f7d 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:
-- 
cgit v1.2.3