aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-compcert.sh4
1 files changed, 3 insertions, 1 deletions
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)')