work around a bug in bash's implementation of "time"

diff --git a/all b/all
index 287dfdced62b10fc1da61d7d20b3c0e7573251d0..e750d9ae491067e7956b23ae63c06a613a5b58cd 100755 (executable)
--- a/all
+++ b/all
@@ -339,11 +339,16 @@ mkzip0()
        zip -0y "$@"
 }
 
        zip -0y "$@"
 }
 

+timewrapper()
+{
+       time -p "$@"
+}
+

 mirrorspeed()
 {
        # first result is to be ignored, but we use it to check status
        git ls-remote "$1" refs/heads/master >/dev/null 2>&1 || return 1
 mirrorspeed()
 {
        # first result is to be ignored, but we use it to check status
        git ls-remote "$1" refs/heads/master >/dev/null 2>&1 || return 1

-       time -p git ls-remote "$1" refs/heads/master 2>&1 >/dev/null | head -n 1 | cut -d ' ' -f 2 | tr -d . | sed 's,^0*,,'
+       timewrapper git ls-remote "$1" refs/heads/master 2>&1 >/dev/null | head -n 1 | cut -d ' ' -f 2 | tr -d . | sed 's,^0*,,'

                # unit: clock ticks (depends on what "time" returns
 }
 
                # unit: clock ticks (depends on what "time" returns
 }