From 22b6d45b8765ba7ab2750753bb7aaa7700c99946 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Jul 2020 14:00:20 +0200
Subject: CI: pass -silent to coqchk in compcert job

Otherwise gitlab stops logging somewhere in the middle.

Also pass -o because we can.
---
 dev/ci/ci-compcert.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 59a85e4726..9cb7a65ab5 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -6,4 +6,6 @@ ci_dir="$(dirname "$0")"
 git_download compcert
 
 ( cd "${CI_BUILD_DIR}/compcert" && \
-  ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
+      ./configure -ignore-coq-version x86_32-linux && \
+      make && \
+      make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)')
-- 
cgit v1.2.3