]> de.git.xonotic.org Git - xonotic/xonotic.git/commitdiff
Fix detection of time.
authorRudolf Polzer <divverent@xonotic.org>
Sat, 18 Jan 2014 13:48:47 +0000 (14:48 +0100)
committerRudolf Polzer <divverent@xonotic.org>
Sat, 18 Jan 2014 13:48:47 +0000 (14:48 +0100)
Apparently, in some shells, time can be only used as a reserved word,
but not as a program/builtin.

misc/tools/all/config.subr

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