diff options
| author | Maxime Dénès | 2016-11-09 16:47:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-10 12:37:02 +0100 |
| commit | 76ed02a6b2e282bf394e083a97047678fe807ad3 (patch) | |
| tree | bd870e830e260208120a8cd15b97c3c0ff05192e /dev/make-installer-win32.sh | |
| parent | 034db0eae27c427a09092c337874c713474f50cb (diff) | |
Remove old windows build scripts.
Diffstat (limited to 'dev/make-installer-win32.sh')
| -rwxr-xr-x | dev/make-installer-win32.sh | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh deleted file mode 100755 index 51d428dd1e..0000000000 --- a/dev/make-installer-win32.sh +++ /dev/null @@ -1,22 +0,0 @@ -#!/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 -URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download - -[ -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/*" - wget -O $ZIP $URL2 && 7z x $ZIP "bin/*" - rm -rf $ZIP -fi -VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2` -cd dev/nsis -"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win32" coq.nsi -echo Installer: -ls -h $PWD/*exe -cd ../.. |