diff options
| author | Théo Zimmermann | 2017-08-12 01:41:40 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-08-12 01:41:40 +0200 |
| commit | 6548d0c05bc7874ac652ad430b0139860a89c551 (patch) | |
| tree | 71c9829d50f54aa91f87e1ec7f40409667aba6cd /tools | |
| parent | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (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.in | 8 |
1 files changed, 4 insertions, 4 deletions
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 |