Bug fixed: removal of .__log was not always attempted.

[helm.git] / helm / matita / scripts / do_tests.sh

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index ad9d18bb19a7ad8ef2e5713e8ac5e16f3ce0c20e..b8df5141895d7c96a59e1c6bb9e292431dc82b2c 100755 (executable)
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -63,9 +63,9 @@ for T in $TODO; do
    else
      diff $LOG `basename $T .ma`.log > $DIFF
      RC=$?
-     rm -f $LOG
    fi
   fi
+  rm -f $LOG
   if [ $RC = 0 ]; then
     printf "$OK\t$TIMES\t$DO_TESTS_EXTRA\n"
   else