From 5239af30618d3c23666cc75078bf269172b6d3df Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 3 Jul 2018 11:34:18 +0200 Subject: Fix timing tools on NixOS. --- tools/CoqMakefile.in | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8e60d3932..7aa2d0a5a 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 -- cgit v1.2.3