src/Tools/rm-logfiles

--- a/src/Tools/rm-logfiles	Tue Apr 15 10:23:38 1997 +0200
+++ b/src/Tools/rm-logfiles	Wed Apr 16 18:13:12 1997 +0200
@@ -1,6 +1,6 @@
 #! /bin/sh
 # $Id$
 #Remove useless files from subdirectories
-rm log */make*.log */make*.log.gz
-rm */test
-rm */.*.thy.ML */*/.*.thy.ML
+
+find . \( -name log -o -name make\*.log\* -o -name test -o -name .\*.thy.ML \) -print \
+  | xargs rm