From 2c7bdd489024ee7ed205870e8086a475bdba53dc Mon Sep 17 00:00:00 2001
From: Jean Privat <jean@pryen.org>
Date: Thu, 25 Sep 2014 20:38:20 -0400
Subject: [PATCH] jenkins: add --quiet to time in unitrun.sh

Signed-off-by: Jean Privat <jean@pryen.org>
---
 misc/jenkins/unitrun.sh |    2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/misc/jenkins/unitrun.sh b/misc/jenkins/unitrun.sh
index bb5b86e..54d875c 100755
--- a/misc/jenkins/unitrun.sh
+++ b/misc/jenkins/unitrun.sh
@@ -26,7 +26,7 @@ shift
 
 # 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 -o "${name}.t.out" "$@" > >(tee "${name}.out") 2> >(tee "${name}.2.out" >&2)
+/usr/bin/time -f%U --quiet -o "${name}.t.out" "$@" > >(tee "${name}.out") 2> >(tee "${name}.2.out" >&2)
 res=$?
 
 c=`echo "${name%-*}" | tr "-" "."`
-- 
1.7.9.5