aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-08-12 01:41:40 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-08-12 01:41:40 +0200
commit6548d0c05bc7874ac652ad430b0139860a89c551 (patch)
tree71c9829d50f54aa91f87e1ec7f40409667aba6cd /tools
parent1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff)
More portable location for the time command.
On NixOS in particular, /usr/bin/time doesn't exist.
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in8
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index e54ea45d4..f43ef295a 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