aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-07-06 12:02:13 -0700
committerGravatar Jason Gross <jagro@google.com>2016-07-06 12:02:13 -0700
commit601886c27382c663d1d9ff910860d6fff50c0705 (patch)
tree0944082fbb1df9071cc5cbe5bf281814dadbfb0d /Makefile
parente6827b29fe19ef1de4b44f26a27820f2e8ecf08e (diff)
Clean up the makefile a bit
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile10
1 files changed, 0 insertions, 10 deletions
diff --git a/Makefile b/Makefile
index d4f168d5b..b6ae6ab61 100644
--- a/Makefile
+++ b/Makefile
@@ -7,16 +7,6 @@ SRC_DIR := src
coqprime coqprime-8.4 coqprime-8.5
.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::