diff options
Diffstat (limited to 'dev/build/windows')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fc8921e63d..ebbf10f548 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -404,8 +404,7 @@ function build_prep { # ------------------------------------------------------------------------------ # Like build_prep, but gets the data from an entry in ci-basic-overlay.sh -# This assumes the following definitions exist in ci-basic-overlay.sh, -# or in a file in the user-overlays folder: +# This assumes the following definitions exist in ci-basic-overlay.sh # $1_CI_REF # $1_CI_ARCHIVEURL # $1_CI_GITURL @@ -432,7 +431,7 @@ function build_prep_overlay { } # ------------------------------------------------------------------------------ -# Load overlay version variables from ci-basic-overlay.sh and user-overlays/*.sh +# Load overlay version variables from ci-basic-overlay.sh # ------------------------------------------------------------------------------ function load_overlay_data { @@ -448,9 +447,6 @@ function load_overlay_data { export CI_PULL_REQUEST="" fi - for overlay in /build/user-overlays/*.sh; do - . "$overlay" - done . /build/ci-basic-overlay.sh } @@ -1204,7 +1200,7 @@ function make_elpi { make_dune make_re - if build_prep https://github.com/LPCIC/elpi/archive v1.11.4 tar.gz 1 elpi; then + if build_prep https://github.com/LPCIC/elpi/archive v1.12.0 tar.gz 1 elpi; then log2 dune build -p elpi log2 dune install elpi @@ -1441,7 +1437,6 @@ function make_coq { # Copy these files somewhere the plugin builds can find them logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ - logn copy-user-overlays cp -r dev/ci/user-overlays /build/ build_post fi @@ -1754,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" |