From 37b6de622f0cf822653d286f6f95e1d828af11ef Mon Sep 17 00:00:00 2001
From: =?utf8?q?Alexis=20Laferri=C3=A8re?= <alexis.laf@xymus.net>
Date: Fri, 24 Oct 2014 07:31:26 -0400
Subject: [PATCH] unitrun: fix use of time command
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

Signed-off-by: Alexis Laferrière <alexis.laf@xymus.net>
---
 misc/jenkins/unitrun.sh |   11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/misc/jenkins/unitrun.sh b/misc/jenkins/unitrun.sh
index 54d875c..10dfd38 100755
--- a/misc/jenkins/unitrun.sh
+++ b/misc/jenkins/unitrun.sh
@@ -24,9 +24,18 @@ fi
 name=$1
 shift
 
+# Detect a working time command
+if env time --quiet -f%U true 2>/dev/null; then
+	TIME="env time --quiet -f%U -o '${name}.t.out'"
+elif env time -f%U true 2>/dev/null; then
+	TIME="env time -f%U -o '${name}.t.out'"
+else
+	TIME=
+fi
+
 # Magic here! This tee and save both stdout and stderr in distinct files without messing with them
 # Time  just get the user time
-/usr/bin/time -f%U --quiet -o "${name}.t.out" "$@" > >(tee "${name}.out") 2> >(tee "${name}.2.out" >&2)
+$TIME "$@" > >(tee "${name}.out") 2> >(tee "${name}.2.out" >&2)
 res=$?
 
 c=`echo "${name%-*}" | tr "-" "."`
-- 
1.7.9.5