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
+
+# Detect a working date command
+if date -Iseconds >/dev/null 2>&1; then
+ TIMESTAMP="timestamp='`date -Iseconds`'"
+else
+ TIMESTAMP=
+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 "-" "."`
n=${name##*-}
+# Do we have a time result?
+if test -f "${name}.t.out"; then
+ T="time='`cat "${name}.t.out"`'"
+else
+ T=
+fi
+
cat > "${name}.xml"<<END
<testsuites><testsuite>
-<testcase classname='$c' name='$n' time='`cat "${name}.t.out"`' timestamp='`date -Iseconds`'>
+<testcase classname='$c' name='$n' $T $TIMESTAMP>
END
if test "$res" != "0"; then
echo >> "${name}.xml" "<error message='Command returned $res'/>"
</testsuite></testsuites>
END
-rm "${name}.out" "${name}.2.out" "${name}.t.out"
+rm "${name}.out" "${name}.2.out" "${name}.t.out" 2> /dev/null || true