diff options
| author | Pierre-Marie Pédrot | 2015-08-22 16:21:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-22 16:21:07 +0200 |
| commit | 2903ee1394118106f1894798f82dc5cf3730675b (patch) | |
| tree | 76a29b8da20b51b48c6a73516a6ae9c107f57afc /dev | |
| parent | 4c202177e7d1a26f3b8bc105a1ceb604f178b584 (diff) | |
| parent | 081a649157d2460c924404cd51b4ba50c23b1956 (diff) | |
Merge branch 'v8.5'
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, 5 insertions, 1 deletions
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh index c6ed2f401d..d405e66cc0 100755 --- a/dev/make-installer-win32.sh +++ b/dev/make-installer-win32.sh @@ -1,5 +1,7 @@ #!/bin/sh +set -e + NSIS="$BASE/NSIS/makensis" ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh index 03fdda4aa1..2f765c1a10 100755 --- a/dev/make-installer-win64.sh +++ b/dev/make-installer-win64.sh @@ -1,5 +1,7 @@ #!/bin/sh +set -e + NSIS="$BASE/NSIS/makensis" ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download @@ -11,7 +13,7 @@ mkdir -p bin32 cp bin/* bin32/ make clean make archclean -( . ${BASE}_64/environ; ./configure -debug -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/*" |