X-Git-Url: http://nitlanguage.org
diff --git a/misc/jenkins/unitrun.sh b/misc/jenkins/unitrun.sh
index 6b1c7f5..c1430da 100755
--- a/misc/jenkins/unitrun.sh
+++ b/misc/jenkins/unitrun.sh
@@ -25,10 +25,12 @@ 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"
+if command time --quiet -f%e true 2>/dev/null; then
+ TIME="command time --quiet -f%e -o ${name}.t.out"
+elif command time -f%e true 2>/dev/null; then
+ TIME="command time -f%e -o ${name}.t.out"
+elif command gtime -f%e true 2>/dev/null; then
+ TIME="command gtime -f%e -o ${name}.t.out"
else
TIME=
fi
@@ -63,13 +65,21 @@ if test "$res" != "0"; then
echo >> "${name}.xml" ""
echo "+ Command returned $res" >&2
fi
+if test -s "${name}.out"; then
cat >> "${name}.xml"<
+END
+fi
+if test -s "${name}.2.out"; then
+cat >> "${name}.xml"<
+END
+fi
+cat >> "${name}.xml"<
END