diff options
| author | Jason Gross | 2017-05-11 11:24:54 -0400 |
|---|---|---|
| committer | Enrico Tassi | 2017-05-23 10:48:28 +0200 |
| commit | 3759772965ba91a56f0a6614c192347fd0283edc (patch) | |
| tree | 94ba710482400486edeb6c5b00196b6c985bdaa2 /tools | |
| parent | 7b56ef80850af8ddf13db35b4cd69f6cf1af3549 (diff) | |
Restore 8.5, 8.6 compatibility of STDTIME, TIMECMD
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index a0cf4b02b8..11d9438fe2 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -62,7 +62,8 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= -TIMECMD?=/usr/bin/time -f "$* (user: %U mem: %M ko)" +TIMECMD?= +STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" # Coq binaries COQC ?= $(TIMER) "$(COQBIN)coqc" @@ -111,7 +112,7 @@ COQDEBUG ?= SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) -TIMER=$(if $(TIMED), $(TIMECMD),) +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) OPT?= |