--- a/rm-logfiles Tue Sep 13 10:42:34 1994 +0200
+++ b/rm-logfiles Tue Sep 13 11:19:38 1994 +0200
@@ -2,6 +2,4 @@
#rm-logfiles: remove useless files from subdirectories
rm log */make*.log */make*.log.gz
rm */test
-rm */.*.thy.ML
-rm */ex/.*.thy.ML
-rm HOL/Subst/.*.thy.ML
+find . -name '.*.thy.ML' -print -exec rm {} \;
--- a/src/Tools/rm-logfiles Tue Sep 13 10:42:34 1994 +0200
+++ b/src/Tools/rm-logfiles Tue Sep 13 11:19:38 1994 +0200
@@ -2,6 +2,4 @@
#rm-logfiles: remove useless files from subdirectories
rm log */make*.log */make*.log.gz
rm */test
-rm */.*.thy.ML
-rm */ex/.*.thy.ML
-rm HOL/Subst/.*.thy.ML
+find . -name '.*.thy.ML' -print -exec rm {} \;