From 3759772965ba91a56f0a6614c192347fd0283edc Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 11 May 2017 11:24:54 -0400
Subject: Restore 8.5, 8.6 compatibility of STDTIME, TIMECMD

---
 tools/CoqMakefile.in | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tools')

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?=
 
-- 
cgit v1.2.3