diff options
| author | Enrico Tassi | 2015-06-29 21:34:11 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-06-29 22:16:07 +0200 |
| commit | 671e556453c1eee335cf788ebc72675f5a7483d8 (patch) | |
| tree | d11a400f2f4209afdf26e3996dfed1ac9ba22ef4 /dev | |
| parent | e39b5b8eaa89950216bca646b5e9ef9b56bea7be (diff) | |
win: compile with -debug
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/make-installer-win32.sh | 2 | ||||
| -rwxr-xr-x | dev/make-installer-win64.sh | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh index ec7cd5773a..c6ed2f401d 100755 --- a/dev/make-installer-win32.sh +++ b/dev/make-installer-win32.sh @@ -5,7 +5,7 @@ ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download -[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no +[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no make -j2 if [ ! -e bin/make.exe ]; then wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh index 73e1fdbeb2..03fdda4aa1 100755 --- a/dev/make-installer-win64.sh +++ b/dev/make-installer-win64.sh @@ -5,13 +5,13 @@ ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download -[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no +[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no make -j2 coqide mkdir -p bin32 cp bin/* bin32/ make clean make archclean -( . ${BASE}_64/environ; ./configure -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs ) +( . ${BASE}_64/environ; ./configure -debug -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs ) cp bin32/coqide* bin/ if [ ! -e bin/make.exe ]; then wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" |