diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-07-19 14:28:45 -0700 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-07-19 14:28:45 -0700 |
| commit | d47273cea29099c296e1b702ab25aa8272ab6831 (patch) | |
| tree | 940f9f34a116aeda7b93bc4e75470bf8292d19f3 /tools/coq_makefile.ml | |
| parent | 522bcd72a567a3ae29162519a9a9736581367251 (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/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 2 |
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"; |