diff options
| author | Maxime Dénès | 2017-08-16 09:42:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:42:21 +0200 |
| commit | f63471f8979f1b43f88c2ddf12a8fcaceb8d1e79 (patch) | |
| tree | 144d1e9ca74d90c25b7d005e495357b419b3a3e4 | |
| parent | ae827f670d8ea405ed06b52ad841cf690ebd18a8 (diff) | |
| parent | 6548d0c05bc7874ac652ad430b0139860a89c551 (diff) | |
Merge PR #964: More portable location for the time command.
| -rw-r--r-- | Makefile.build | 10 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 8 |
2 files changed, 9 insertions, 9 deletions
diff --git a/Makefile.build b/Makefile.build index b45c6427a1..3d4b475dcd 100644 --- a/Makefile.build +++ b/Makefile.build @@ -31,7 +31,7 @@ TIMED ?= # When $(TIMED) is set, the time command used by default is $(STDTIME) # (see below), unless the following variable is non-empty. For instance, -# it could be set to "'/usr/bin/time -p'". +# it could be set to "'/usr/bin/env time -p'". TIMECMD ?= # When non-empty, -time is passed to coqc and the output is recorded @@ -167,11 +167,11 @@ DEPENDENCIES := \ ########################################################################### # Default timing command -# 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) @@ -180,7 +180,7 @@ STDTIME?=time endif endif else -STDTIME?=/usr/bin/time -f $(TIMEFMT) +STDTIME?=/usr/bin/env time -f $(TIMEFMT) endif TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 3a8ca7b8d6..9f891afe53 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 |