diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/make-installer-win32.sh | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh index acbcb040bc..fce119f779 100755 --- a/dev/make-installer-win32.sh +++ b/dev/make-installer-win32.sh @@ -12,9 +12,6 @@ if [ ! -e bin/make.exe ]; then wget -O $ZIP $URL2 && 7z x $ZIP "bin/*" rm -rf $ZIP fi -ocamlc unix.cma tools/mkwinapp.ml -o bin/mkwinapp.exe -bin/mkwinapp.exe bin/coqide.exe -bin/mkwinapp.exe bin/coqide.byte.exe VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2` cd dev/nsis "$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi |