diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-16 12:12:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-16 12:12:35 +0200 |
| commit | 63aaabd93d32a4982803daff44900ecb0acb5b76 (patch) | |
| tree | 55c70c4b13ce44321936ff7157381d13e4311e15 | |
| parent | 68d5c06ba59fa57037826b2286d3086bf57d79db (diff) | |
| parent | d47273cea29099c296e1b702ab25aa8272ab6831 (diff) | |
Merge PR #250 into v8.6
| -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"; |