From 31098bfe8fa98a072330b851afb3a4f0916527ab Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 9 Jun 2017 17:52:48 -0400
Subject: Fix TIMED=1 on Mac OSX

This closes [bug #5596](https://coq.inria.fr/bugs/show_bug.cgi?id=5596).
---
 tools/CoqMakefile.in | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 86be54d462..e4f527d445 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -62,7 +62,21 @@ VERBOSE ?=
 # Time the Coq process (set to non empty), and how (see default value)
 TIMED?=
 TIMECMD?=
-STDTIME?=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+# Use /usr/bin/time on linux, gtime on Mac OS
+TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+ifneq (,$(TIMED))
+ifeq (0,$(shell /usr/bin/time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=/usr/bin/time -f $(TIMEFMT)
+else
+ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=gtime -f $(TIMEFMT)
+else
+STDTIME?=time
+endif
+endif
+else
+STDTIME?=/usr/bin/time -f $(TIMEFMT)
+endif
 
 # Coq binaries
 COQC     ?= "$(COQBIN)coqc"
-- 
cgit v1.2.3