diff options
| author | Enrico Tassi | 2014-09-17 12:01:19 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-17 14:55:07 +0200 |
| commit | 676fd439fd98f71100ffcf5306dcb7704cd11e79 (patch) | |
| tree | 573fa98c1b971b2bf1025de72bb7298e07e006ca /dev | |
| parent | a4ad14610cc0baab46264b179c4b8057f40d52c7 (diff) | |
win32: use subsystem windows on windows (and not console)
This makes the hammer tools/mkwinapp.ml kind of obsolete
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 |