diff options
Diffstat (limited to 'dev/build')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 0dcabc0b97..d0b5f4be47 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1076,7 +1076,7 @@ function make_ocaml { function make_ocaml_tools { make_findlib - make_camlp5 + # make_camlp5 } ##### OCAML EXTRA LIBRARIES ##### @@ -1386,7 +1386,7 @@ function make_coq { make_ocaml make_num make_findlib - make_camlp5 + # make_camlp5 make_lablgtk if case $COQ_VERSION in |