--- a/src/Tools/rm-logfiles Fri Nov 08 14:02:51 1996 +0100
+++ b/src/Tools/rm-logfiles Fri Nov 08 14:04:38 1996 +0100
@@ -3,4 +3,4 @@
#Remove useless files from subdirectories
rm log */make*.log */make*.log.gz
rm */test
-rm */.*.thy.ML */.*.thy.ML */*/.*.thy.ML
+rm */.*.thy.ML */*/.*.thy.ML