diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-compcert.sh | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 6f6b3cd6d2..6cc91ace81 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1749,7 +1749,7 @@ function make_addon_compcert { installer_addon_dependency_end if build_prep_overlay compcert; then installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off" - logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin + logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin -use-external-MenhirLib -use-external-Flocq log1 make $MAKE_OPT log2 make install logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE" 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)') |