diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-07-11 16:16:20 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-07-11 18:22:54 +0200 |
| commit | 3986eabe91a1b2b9280a711d1de86f331985c158 (patch) | |
| tree | ad68158ae5f9a8d420954e06ce51a6d10be6e498 /Makefile.build | |
| parent | 52fee346200228d8fa05f1708bb85233f12c7b81 (diff) | |
Removing "VERBOSE=" from "Makefile.build"
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index ebf2996f1..719046f99 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) |