From 6dd20891217d00ac86f1d680f4e967b61bc596e4 Mon Sep 17 00:00:00 2001 From: Rudolf Polzer Date: Sat, 18 Jan 2014 14:48:47 +0100 Subject: [PATCH 1/1] Fix detection of time. Apparently, in some shells, time can be only used as a reserved word, but not as a program/builtin. --- misc/tools/all/config.subr | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/misc/tools/all/config.subr b/misc/tools/all/config.subr index cb07d15e..1c560fa9 100644 --- a/misc/tools/all/config.subr +++ b/misc/tools/all/config.subr @@ -35,7 +35,10 @@ allmirrors() "$@" ssh push ssh://xonotic@push.git.xonotic.org/ '' } -time= -if { time -p sh -c 'true'; } 2>&1 >/dev/null | grep '^user ' >/dev/null; then - time="time -p" +time="time -p" +if { $time sh -c 'true'; } 2>&1 >/dev/null | grep '^user ' >/dev/null; then + msg "Timing via the time utility works." +else + time= + msg "Timing not supported." fi -- 2.39.2