Fixes issue #7172 (don't include MinGW make in install)

3 files changed, 36 insertions, 6 deletions

diff --git a/dev/build/windows/MakeCoq_88git_installer.bat b/dev/build/windows/MakeCoq_88git_installer.bat
new file mode 100755
index 000000000..b016fb389
--- /dev/null
+++ b/dev/build/windows/MakeCoq_88git_installer.bat
@@ -0,0 +1,27 @@
+@ECHO OFF

+

+REM ========== COPYRIGHT/COPYLEFT ==========

+

+REM (C) 2016 Intel Deutschland GmbH

+REM Author: Michael Soegtrop

+

+REM Released to the public by Intel under the

+REM GNU Lesser General Public License Version 2.1 or later

+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html

+

+REM ========== BUILD COQ ==========

+

+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -installer=Y ^

+  -coqver=git-v8.8 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_88_inst ^

+  -destcoq=%ROOTPATH%\coq64_88_inst ^

+  -addon=bignums

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_88git_installer.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index ccf22cc86..f960ff008 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -34,7 +34,7 @@ REM see -ocaml in ReadMe.txt
 SET INSTALLOCAML=N
 
 REM see -make in ReadMe.txt
-SET INSTALLMAKE=Y
+SET INSTALLMAKE=N
 
 REM see -destcyg in ReadMe.txt
 SET DESTCYG=C:\bin\cygwin_coq
@@ -267,7 +267,6 @@ IF "%INSTALLMODE%" == "mingwincygwin" (
 IF "%MAKEINSTALLER%" == "Y" (
   SET INSTALLMODE=relocatable
   SET INSTALLOCAML=Y
-  SET INSTALLMAKE=Y
 )
 
 REM ========== CONFIRM PARAMETERS ==========
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 8e0d2341d..918900ccb 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -142,18 +142,22 @@ LOGS=`pwd`/buildlogs
 # The current log target (first part of the log file name)
 LOGTARGET=other
 
+# Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
 log1() {
   "$@" > $LOGS/$LOGTARGET-$1.log 2> $LOGS/$LOGTARGET-$1.err
 }
 
+# Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
 log2() {
   "$@" > $LOGS/$LOGTARGET-$1-$2.log 2> $LOGS/$LOGTARGET-$1-$2.err
 }
 
+# Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
 log_1_3() {
   "$@" > $LOGS/$LOGTARGET-$1-$3.log 2> $LOGS/$LOGTARGET-$1-$3.err
 }
 
+# Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
 logn() {
   LOGTARGETEX=$1
   shift
@@ -1281,7 +1285,6 @@ function get_cygwin_mingw_sources {
 
 function make_coq_installer {
   make_coq
-  make_mingw_make
   get_cygwin_mingw_sources
 
   # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build:
@@ -1334,12 +1337,13 @@ function make_coq_installer {
 }
 
 ###################### ADDONS #####################
+
 function make_addon_bignums {
-  if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1; then
+  if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1 bignums-8.8+beta1; then
     # To make command lines shorter :-(
     echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
-    logn make make all
-    logn make-install make install
+    log1 make all
+    log2 make install
     build_post
   fi
 }