# HG changeset patch
# User paulson
# Date 847190889 -3600
# Node ID c25714ca1c197883a0a45ec2afb2663a5195ce12
# Parent  ad4382e546fccc1f000f575415449255b95979e4
Replaced the very slow "find" command by "rm" with wildcards

diff -r ad4382e546fc -r c25714ca1c19 src/Tools/rm-logfiles
--- a/src/Tools/rm-logfiles	Tue Nov 05 11:20:52 1996 +0100
+++ b/src/Tools/rm-logfiles	Tue Nov 05 11:48:09 1996 +0100
@@ -3,4 +3,4 @@
 #Remove useless files from subdirectories
 rm log */make*.log */make*.log.gz
 rm */test
-find . -name '.*.thy.ML' -print -exec rm {} \;
+rm */.*.thy.ML */.*.thy.ML */*/.*.thy.ML