__ files are removed

diff --git a/helm/matita/contribs/LAMBDA-TYPES/Makefile b/helm/matita/contribs/LAMBDA-TYPES/Makefile
index 297b5cb9c1420d543262edd864033c8a543579fe..5e651970a0fbf8be681cb3eb66b9e8d81e317909 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/matita/contribs/LAMBDA-TYPES/Makefile
@@ -32,10 +32,13 @@ verbose:
 %.opt:
        $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
 
-clean:
+clean_:
+       rm -r __*not_for_matita
+
+clean: clean_
        $(H)$(MATITACLEAN) $(SRC)
 
-cleanall:
+cleanall: clean_
        $(H)rm -f $(SRC:%.ma=%.moo)
        $(MATITACLEAN) all
 

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
index c12b0fb43fc2328504fc16b1d0a15cdb13515ea9..43221d3caa9719f4cd078259a984a2b8ca15304b 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
@@ -32,10 +32,13 @@ verbose:
 %.opt:
        $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
 
-clean:
+clean_:
+       rm -r __*not_for_matita
+
+clean: clean_
        $(H)$(MATITACLEAN) $(SRC)
 
-cleanall:
+cleanall: clean_
        $(H)rm -f $(SRC:%.ma=%.moo)
        $(MATITACLEAN) all
 

diff --git a/helm/matita/library/Makefile b/helm/matita/library/Makefile
index e13b3e8a48d6c05fb5e07f19043e285192c24309..b6d061531b84332ff0a362b86482e5c98f186e38 100644 (file)
--- a/helm/matita/library/Makefile
+++ b/helm/matita/library/Makefile
@@ -32,7 +32,10 @@ verbose:
 %.opt:
        $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
 
-clean:
+clean_:
+       rm -f __*not_for_matita
+
+clean: clean_
        $(H)$(MATITACLEAN) $(SRC)
 
 cleanall:

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index b7500bf03a3d0e3cb59d41cf5a6a5b6e57c592cb..687b7f8c07b928bb0afae68f628672e7aa3cc8b9 100755 (executable)
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -12,6 +12,10 @@ if [ "$1" = "-twice" ]; then
   shift
   TWICE=1
 fi
+if [ "$1" = "-keep-logs" ]; then
+  shift
+  KEEP=1
+fi
 
 COMPILER=$1
 shift
@@ -27,11 +31,12 @@ TODO="$@"
 if [ -z "$COMPILER" -o -z "$CLEANER" -o -z "$LOGFILE" -o -z "$EXPECTED" -o -z "$TODO" ]; then
   echo
   echo "usage: "
-  echo "  do_tests.sh [-no-color] [-twice] ./compiler ./cleaner logfile expected_result test.ma ..."
+  echo "  do_tests.sh [-no-color] [-twice] [-keep-logs] ./compiler ./cleaner logfile expected_result test.ma ..."
   echo
   echo "options:  "
   echo "  -no-color Do not use vt100 colors"
   echo "  -twice    Run each test twice but show only the second run times"
+  echo "  -keep-logs Do not dele __* files"
   echo
   echo "If expected_result is OK the result will be OK if the test compiles."
   echo "Otherwise if expected_result is FAIL the result will be OK if the test"
@@ -72,7 +77,9 @@ for T in $TODO; do
     printf "$FAIL\t$TIMES\t$DO_TESTS_EXTRA\n";
     cat $DIFF
   fi
-  #rm -f $LOG
-  #rm -f $DIFF
+  if [ "$KEEP" != "1" ]; then
+    rm -f $LOG
+    rm -f $DIFF
+  fi
   exit $RC
 done

diff --git a/helm/matita/scripts/profile_cvs.sh b/helm/matita/scripts/profile_cvs.sh
index 667a70e36de142e1b25987104ee1911ee0d43106..40e19b841eafd94186a094e8fc14096ac87edadf 100755 (executable)
--- a/helm/matita/scripts/profile_cvs.sh
+++ b/helm/matita/scripts/profile_cvs.sh
@@ -7,8 +7,8 @@ function testit {
   LOGTOOPT=/dev/null
   LOGTOBYTE=/dev/null
   export DO_TESTS_EXTRA="$MARK\t$@"
-  make tests DO_TESTS_OPTS="-no-color -twice"
-  make tests.opt DO_TESTS_OPTS="-no-color -twice"
+  make tests DO_TESTS_OPTS="-no-color -twice -keep-logs"
+  make tests.opt DO_TESTS_OPTS="-no-color -twice -keep-logs"
 }
 
 function compile {

diff --git a/helm/matita/tests/Makefile b/helm/matita/tests/Makefile
index 1ea16550dffe1a7bc0673aa652c4a613d5c2ff0c..ee1f6bbe99895fcd676978af3d71a8ce5acfedf2 100644 (file)
--- a/helm/matita/tests/Makefile
+++ b/helm/matita/tests/Makefile
@@ -32,10 +32,13 @@ verbose:
 %.opt:
        $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
 
-clean:
+clean_:
+       rm -r __*not_for_matita
+
+clean: clean_
        $(H)$(MATITACLEAN) $(SRC)
 
-cleanall:
+cleanall: clean_
        $(H)rm -f $(SRC:%.ma=%.moo)
        $(MATITACLEAN) all
 

diff --git a/helm/matita/tests/bad_tests/Makefile b/helm/matita/tests/bad_tests/Makefile
index 19ff97412bf6245017bb7a10a1c65bdeda94ba6d..1b955ff184597b0c65405b2e1bf46d26ab25b2ac 100644 (file)
--- a/helm/matita/tests/bad_tests/Makefile
+++ b/helm/matita/tests/bad_tests/Makefile
@@ -32,10 +32,13 @@ verbose:
 %.opt:
        $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
 
-clean:
+clean_:
+       rm -r __*not_for_matita
+
+clean: clean_
        $(H)$(MATITACLEAN) $(SRC)
 
-cleanall:
+cleanall: clean_
        $(H)rm -f $(SRC:%.ma=%.moo)
        $(MATITACLEAN) all