From df7f4445e73d7b47a3964fa477c533e6084eaa6f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 4 Sep 2017 16:11:14 +0200 Subject: Remove -debug option from Windows build script. It is no longer accepted by Coq's ./configure. --- dev/build/windows/makecoq_mingw.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dev/build') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fd5f47d0f..f3e4cec0b 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1124,11 +1124,11 @@ function make_coq { then if [ "$INSTALLMODE" == "relocatable" ]; then # HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path - ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man + ./configure -with-doc no -prefix ./ -libdir ./lib -mandir ./man elif [ "$INSTALLMODE" == "absolute" ]; then - ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" + ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" else - ./configure -debug -with-doc no -prefix "$PREFIXCOQ" + ./configure -with-doc no -prefix "$PREFIXCOQ" fi # The windows resource compiler binary name is hard coded @@ -1143,7 +1143,7 @@ function make_coq { fi if [ "$INSTALLMODE" == "relocatable" ]; then - ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" + ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" fi make install -- cgit v1.2.3