From dc8e605d9cadf0d7ead78481e0e68756713f7aa0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 24 Nov 2020 09:46:54 +0100
Subject: [ci] make compcert use flocq and menhir

---
 dev/ci/ci-compcert.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/ci/ci-compcert.sh')

diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 6b09726606..3c8d65f5c1 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -7,6 +7,6 @@ git_download compcert
 
 export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
 ( cd "${CI_BUILD_DIR}/compcert" && \
-      ./configure -ignore-coq-version x86_32-linux && \
+      ./configure -ignore-coq-version x86_32-linux -use-external-MenhirLib -use-external-Flocq && \
       make && \
       make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)')
-- 
cgit v1.2.3