- /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"
+ TIMES=`(time $COMPILER $T > $LOG 2>&1) 2>&1`
+ RC=$?;
+ cat $LOG >> $LOGFILE
+ touch $DIFF
+ if [ $EXPECTED = "FAIL" ]; then
+ if [ $RC = 0 ]; then
+ echo "The test was successful but it should have failed!" > $DIFF
+ RC=1;
+ else
+ diff $LOG `basename $T .ma`.log > $DIFF
+ RC=$?
+ fi
+ fi
+ rm -f $LOG
+ if [ $RC = 0 ]; then
+ printf "$OK\t$TIMES\t$DO_TESTS_EXTRA\n"