one more try

[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 1e27df81aa58ff4164bb9cb7db64c326b776dbba..b7500bf03a3d0e3cb59d41cf5a6a5b6e57c592cb 100755 (executable)
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -44,7 +44,7 @@ fi
 
 export TIMEFORMAT="%2lR %2lU %2lS"
 for T in $TODO; do
-  TT=`echo $T | sed s?/?.?`
+  TT=`echo $T | sed s?/?.?`.not_for_matita
   LOG=__log_$TT
   DIFF=__diff_$TT
   printf "$CLEANCOMPILER\t%-30s   " $T