From 951f80b0ce46976791d8b7fa7cf68aea11018da0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 2 Mar 2018 17:53:47 +0100
Subject: build: win: turn off build/installation of gnu Make

---
 dev/build/windows/makecoq_mingw.sh | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'dev/build')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index b0801190e1..49eece5a44 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1361,10 +1361,7 @@ list_files ocaml
 make_coq
 
 if [ "$INSTALLMAKE" == "Y" ] ; then
-  # I've to comment this out becase, with addons, if this make is in the
-  # PATH it hides the real one (the one that works, while this one does not)
-  #make_mingw_make
-  :
+  make_mingw_make
 fi
 
 list_files ocaml_coq
-- 
cgit v1.2.3