# 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