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