Merge PR#742: Fix `make TIMED=1` garbage

1 files changed, 21 insertions, 22 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 5e223a0b4..7b01c1b66 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -5,7 +5,7 @@
 ##    //   #                                                                 ##
 ###############################################################################
 ## GNUMakefile for Coq @COQ_VERSION@
-  
+
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
 # To implement recursion we save the name of the main Makefile
@@ -65,8 +65,8 @@ TIMECMD?=
 STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 
 # Coq binaries
-COQC     ?= $(TIMER) "$(COQBIN)coqc"
-COQCHK   ?= $(TIMER) "$(COQBIN)coqchk"
+COQC     ?= "$(COQBIN)coqc"
+COQCHK   ?= "$(COQBIN)coqchk"
 COQDEP   ?= "$(COQBIN)coqdep"
 GALLINA  ?= "$(COQBIN)gallina"
 COQDOC   ?= "$(COQBIN)coqdoc"
@@ -80,7 +80,7 @@ CAMLOPTLINK ?= $(OCAMLFIND) opt       -rectypes -thread
 CAMLDEP     ?= $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
 
 # DESTDIR is prepended to all installation paths
-DESTDIR ?= 
+DESTDIR ?=
 
 # Debug builds, typically -g to OCaml, -debug to Coq.
 CAMLDEBUG ?=
@@ -96,7 +96,7 @@ COQDEBUG ?=
 #
 # post-all::
 # 	echo "All done!"
-# 
+#
 # in @LOCAL_FILE@
 #
 ###############################################################################
@@ -106,7 +106,7 @@ COQDEBUG ?=
 
 # Flags #######################################################################
 #
-# We define a bunch of variables combining the parameters 
+# We define a bunch of variables combining the parameters
 
 SHOW := $(if $(VERBOSE),@true "",@echo "")
 HIDE := $(if $(VERBOSE),,@)
@@ -127,7 +127,7 @@ DYNLIB:=.cmxs
 endif
 
 COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
-COQCHKFLAGS?=-silent -o $(COQLIBS) 
+COQCHKFLAGS?=-silent -o $(COQLIBS)
 COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML)
 
 # The version of Coq being run and the version of coq_makefile that
@@ -155,7 +155,7 @@ COQLIBINSTALL = $(COQLIB)user-contrib
 COQDOCINSTALL = $(DOCDIR)user-contrib
 COQTOPINSTALL = $(COQLIB)toploop
 
-# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) 
+# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not)
 ifneq "$(DSTROOT)" ""
 DESTDIR := $(DSTROOT)
 endif
@@ -248,7 +248,7 @@ ALLDFILES = $(addsuffix .d,$(ALLSRCFILES))
 
 # Compilation targets #########################################################
 
-all: 
+all:
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
@@ -281,17 +281,17 @@ quick: $(VOFILES:.vo=.vio)
 .PHONY: quick
 
 vio2vo:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) \
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
 		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: vio2vo
 
 checkproofs:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) \
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
 		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: checkproofs
 
 validate: $(VOFILES)
-	$(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=))
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=))
 .PHONY: validate
 
 only: $(TGTS)
@@ -427,10 +427,10 @@ clean::
 	$(HIDE)rm -f $(CMOFILES)
 	$(HIDE)rm -f $(CMIFILES)
 	$(HIDE)rm -f $(CMAFILES)
-	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx) 
+	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
 	$(HIDE)rm -f $(CMXAFILES)
-	$(HIDE)rm -f $(CMXSFILES) 
-	$(HIDE)rm -f $(CMOFILES:.cmo=.o) 
+	$(HIDE)rm -f $(CMXSFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
 	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
 	$(HIDE)rm -f $(ALLDFILES)
 	$(HIDE)rm -f $(ALLNATIVEFILES)
@@ -513,26 +513,26 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
 	$(SHOW)'CAMLOPT -pack -o $@'
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
 
-# This rule is for _CoqProject with no .mllib nor .mlpack 
+# This rule is for _CoqProject with no .mllib nor .mlpack
 $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
 	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $<
 
 $(VOFILES): %.vo: %.v
 	$(SHOW)COQC $<
-	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
 
 # FIXME ?merge with .vo / .vio ?
 $(GLOBFILES): %.glob: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
 
 $(VFILES:.v=.vio): %.vio: %.v
 	$(SHOW)COQC -quick $<
-	$(HIDE)$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
 
 $(BEAUTYFILES): %.v.beautified: %.v
 	$(SHOW)'BEAUTIFY $<'
-	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
 
 $(GFILES): %.g: %.v
 	$(SHOW)'GALLINA $<'
@@ -600,7 +600,7 @@ byte:
 
 opt:
 	$(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
-.PHONY:	opt 
+.PHONY:	opt
 
 # This is deprecated.  To extend this makefile use
 # extension points and @LOCAL_FILE@
@@ -655,4 +655,3 @@ debug:
 .PHONY: debug
 
 .DEFAULT_GOAL := all
-