aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-06-16 17:32:25 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-06-16 17:32:25 -0400
commit7dc373e4c82f3e7a37832321abc9057cb55348f2 (patch)
treec9df60e9abca4e88034d200fbd28b66c54f17b36 /Makefile
parent94fc77bb39af399a0d1256fccdc11b90c0d00cb5 (diff)
Be a bit more quiet on make unless VERBOSE=1 is passed
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile16
1 files changed, 14 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 5fb1ab33c..48f8a9d5b 100644
--- a/Makefile
+++ b/Makefile
@@ -4,10 +4,21 @@ SRC_DIR := src
.PHONY: coq clean install coqprime-8.4 coqprime-8.5 coqprime update-_CoqProject
.DEFAULT_GOAL := coq
+VERBOSE = 0
+
+SILENCE_COQC_0 = @echo "COQC $<"; #
+SILENCE_COQC_1 =
+SILENCE_COQC = $(SILENCE_COQC_$(VERBOSE))
+
+SILENCE_COQDEP_0 = @echo "COQDEP $<"; #
+SILENCE_COQDEP_1 =
+SILENCE_COQDEP = $(SILENCE_COQDEP_$(VERBOSE))
+
SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
update-_CoqProject::
- (echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R Bedrock Bedrock'; (git ls-files 'src/*.v' 'Bedrock/*.v' | $(SORT_COQPROJECT))) > _CoqProject
+ $(VECHO) "GIT LS-FILES *.V > _COQPROJECT"
+ $(Q)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R Bedrock Bedrock'; (git ls-files 'src/*.v' 'Bedrock/*.v' | $(SORT_COQPROJECT))) > _CoqProject
coq: coqprime Makefile.coq
$(MAKE) -f Makefile.coq
@@ -28,7 +39,8 @@ coqprime-8.5:
$(MAKE) -C coqprime-8.5
Makefile.coq: Makefile _CoqProject
- $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+ $(VECHO) "COQ_MAKEFILE"
+ $(Q)$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
clean: Makefile.coq
$(MAKE) -f Makefile.coq clean