X-Git-Url: http://nitlanguage.org diff --git a/misc/jenkins/unitrun.sh b/misc/jenkins/unitrun.sh index 10dfd38..6b1c7f5 100755 --- a/misc/jenkins/unitrun.sh +++ b/misc/jenkins/unitrun.sh @@ -26,13 +26,20 @@ 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'" + 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'" + 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 $TIME "$@" > >(tee "${name}.out") 2> >(tee "${name}.2.out" >&2) @@ -41,9 +48,16 @@ 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 if test "$res" != "0"; then echo >> "${name}.xml" "" @@ -60,4 +74,4 @@ cat >> "${name}.xml"< END -rm "${name}.out" "${name}.2.out" "${name}.t.out" +rm "${name}.out" "${name}.2.out" "${name}.t.out" 2> /dev/null || true