From 3986eabe91a1b2b9280a711d1de86f331985c158 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 11 Jul 2016 16:16:20 +0200
Subject: Removing "VERBOSE=" from "Makefile.build"

---
 Makefile.build | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index ebf2996f10..719046f990 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -59,7 +59,13 @@ DEPENDENCIES := \
 
 # Variables meant to be modifiable via the command-line of make
 
-VERBOSE=
+# If you do:
+#
+#   VERBOSE=1 make
+#
+# then instead of shortened version of the commands run by make
+# you will see the actual commands.
+
 NO_RECOMPILE_ML4=
 NO_RECALC_DEPS=
 READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
@@ -90,8 +96,13 @@ BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 # or only abbreviated versions. 
 # Quiet mode is ON by default except if VERBOSE=1 option is given to make
 
-SHOW := $(if $(VERBOSE),@true "",@echo "")
-HIDE := $(if $(VERBOSE),,@)
+ifdef VERBOSE
+SHOW := @true ""
+HIDE :=
+else
+SHOW := @echo ""
+HIDE := @
+endif
 
 LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
-- 
cgit v1.2.3