diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-08-17 16:35:06 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-08-17 16:35:15 +0200 |
| commit | 8a22b549e61a1fc120b20a5b220764df6c49b3f8 (patch) | |
| tree | 91c5bd8e23d2944f5947a216395cc54ada5f2fb2 /dev | |
| parent | 369a0c9354497639d96ba2fef94c920e051d00fb (diff) | |
windows build scripts made more accurate in detecting failures
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 c6ed2f401..d405e66cc 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 03fdda4aa..2f765c1a1 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/*" |