# HG changeset patch
# User lcp
# Date 779447978 -7200
# Node ID 245633e2fd572e6cb1236346683064eaae84ff7a
# Parent  72fc777dbda04f965353c2a151574bf20d4a2763
now uses find to locate .thy.ML files everywhere

diff -r 72fc777dbda0 -r 245633e2fd57 rm-logfiles
--- 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 {} \;
diff -r 72fc777dbda0 -r 245633e2fd57 src/Tools/rm-logfiles
--- 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 {} \;