From 0528c147a9eee25668252537905d0c09ec20e3cd Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 13 Sep 2015 11:18:11 +0200
Subject: Coq_makefile: read TIMED and TIMECMD from environment.

Useful e.g. with submakefiles.
---
 tools/coq_makefile.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4b92d57082..b21845aea6 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -508,7 +508,7 @@ let parameters () =
   print "define donewline\n\n\nendef\n";
   print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n";
   print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
-  print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
+  print "TIMED?=\nTIMECMD?=\nSTDTIME=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
   print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
   print "vo_to_obj = $(addsuffix .o,\\\n";
   print "  $(filter-out Warning: Error:,\\\n";
-- 
cgit v1.2.3