diff options
| author | Maxime Dénès | 2015-09-13 11:18:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-09-13 11:23:46 +0200 |
| commit | 0528c147a9eee25668252537905d0c09ec20e3cd (patch) | |
| tree | db289c8a5eb1183204a12e730c1bd34a64858908 /tools | |
| parent | 7df0761305778270fe569c0942e7079a803d57e9 (diff) | |
Coq_makefile: read TIMED and TIMECMD from environment.
Useful e.g. with submakefiles.
Diffstat (limited to 'tools')
| -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 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"; |