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 cb07d15ea8c1f8e24f00e07c63fb6f6cdb8775f0..1c560fa97c06777259ba058819ddef7023f9630a 100644 (file)
--- 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