From 6548d0c05bc7874ac652ad430b0139860a89c551 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 12 Aug 2017 01:41:40 +0200
Subject: More portable location for the time command.

On NixOS in particular, /usr/bin/time doesn't exist.
---
 tools/CoqMakefile.in | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index e54ea45d41..f43ef295aa 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -63,11 +63,11 @@ VERBOSE ?=
 # Time the Coq process (set to non empty), and how (see default value)
 TIMED?=
 TIMECMD?=
-# Use /usr/bin/time on linux, gtime on Mac OS
+# Use /usr/bin/env 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)
+ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=/usr/bin/env time -f $(TIMEFMT)
 else
 ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
 STDTIME?=gtime -f $(TIMEFMT)
@@ -76,7 +76,7 @@ STDTIME?=time
 endif
 endif
 else
-STDTIME?=/usr/bin/time -f $(TIMEFMT)
+STDTIME?=/usr/bin/env time -f $(TIMEFMT)
 endif
 
 # Coq binaries
-- 
cgit v1.2.3