From 601886c27382c663d1d9ff910860d6fff50c0705 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Wed, 6 Jul 2016 12:02:13 -0700
Subject: Clean up the makefile a bit

---
 Makefile | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'Makefile')

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::
-- 
cgit v1.2.3