diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-04 16:11:14 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-05 17:12:00 +0200 |
| commit | df7f4445e73d7b47a3964fa477c533e6084eaa6f (patch) | |
| tree | 1737956abfb56d703023418c4004e244719f3611 /dev/build | |
| parent | 802af9272442815012532818cffb6908ad5707e1 (diff) | |
Remove -debug option from Windows build script.
It is no longer accepted by Coq's ./configure.
Diffstat (limited to 'dev/build')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 8 |
1 files changed, 4 insertions, 4 deletions
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 |