From 843df88cd5b30d7c5ff744735baaea2c5a03a1c5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Wed, 19 Jul 2017 17:59:38 +0200
Subject: Print Coq build output.

---
 dev/build/windows/makecoq_mingw.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/build')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index e17923951..45a5a5a4f 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1134,7 +1134,7 @@ function make_coq {
     if [[ $COQ_VERSION == 8.4* ]] ; then
       log1 make
     else
-      log1 make $MAKE_OPT
+      make $MAKE_OPT
     fi
     
     if [ "$INSTALLMODE" == "relocatable" ]; then
-- 
cgit v1.2.3