Fix detection of time.

Apparently, in some shells, time can be only used as a reserved word,
but not as a program/builtin.
This commit is contained in:
Rudolf Polzer 2014-01-18 14:48:47 +01:00
parent 521c084061
commit 6dd2089121

View 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