From 76ed02a6b2e282bf394e083a97047678fe807ad3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 9 Nov 2016 16:47:52 +0100
Subject: Remove old windows build scripts.

---
 dev/make-installer-win32.sh | 22 ----------------------
 1 file changed, 22 deletions(-)
 delete mode 100755 dev/make-installer-win32.sh

(limited to 'dev/make-installer-win32.sh')

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 ../..
-- 
cgit v1.2.3