- /usr/bin/time --quiet -o $TMP -f "%E\t%U\t%S" $COMPILER $T >> $LOGFILE 2>&1
- if [ $? = 0 ]; then
- echo -e "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA"
+ $CLEANER $T 1>/dev/null 2>/dev/null
+ /usr/bin/time --quiet -o $TMP -f "%E %U %S" $COMPILER $T >> $LOGFILE 2>&1
+ RC=$?;
+ if [ $RC = 0 ]; then
+ printf "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA\n"
+ rm $TMP