From: Rudolf Polzer <divverent@xonotic.org>
Date: Sat, 18 Jan 2014 13:48:47 +0000 (+0100)
Subject: Fix detection of time.
X-Git-Tag: xonotic-v0.8.0~45
X-Git-Url: http://git.xonotic.org/?p=xonotic%2Fxonotic.git;a=commitdiff_plain;h=6dd20891217d00ac86f1d680f4e967b61bc596e4;hp=521c08406137d3ea1c92fcf401430306166c4b50

Fix detection of time.

Apparently, in some shells, time can be only used as a reserved word,
but not as a program/builtin.
---

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