# HG changeset patch
# User wenzelm
# Date 861207192 -7200
# Node ID 92599a47a7ab1f2765e2ce310b90f7a5a96cf2ec
# Parent  a16e1011bcc1eb38ad937dfec3ae5f8ec5be24ac
improved;

diff -r a16e1011bcc1 -r 92599a47a7ab 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