aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Jason Gross <jasongross9@gmail.com>2016-07-19 14:28:45 -0700
committerGravatar GitHub <noreply@github.com>2016-07-19 14:28:45 -0700
commitd47273cea29099c296e1b702ab25aa8272ab6831 (patch)
tree940f9f34a116aeda7b93bc4e75470bf8292d19f3 /tools
parent522bcd72a567a3ae29162519a9a9736581367251 (diff)
Allow `STDTIME=foo make`
This gives better behavior both when including the `coq_makefile` `Makefile` into other `Makefile`s and when setting `STDTIME` through an environment variable.
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b86df7c80..ac69a69a4 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -582,7 +582,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";