diff options
| author | Gaëtan Gilbert | 2018-07-04 23:30:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-04 23:30:43 +0200 |
| commit | 90a4afc3742b31fc6ebbbbe4b5383663f65a5788 (patch) | |
| tree | b558e94c25e8f79e51adf82b8d7033daf1d3c618 /tools | |
| parent | 00b23680d55765d9c681751813ab6e85d41786c5 (diff) | |
| parent | def875bd55053957fb28bc6004576b6ca20dad7a (diff) | |
Merge PR #7973: Add a test build on NixOS to GitLab CI.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8e60d3932a..7aa2d0a5a5 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -65,20 +65,20 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -# Use /usr/bin/env time on linux, gtime on Mac OS +# Use command time on linux, gtime on Mac OS TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) else ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else -STDTIME?=time +STDTIME?=command time endif endif else -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +STDTIME?=command time -f $(TIMEFMT) endif # Coq binaries |