# HG changeset patch
# User paulson
# Date 847458278 -3600
# Node ID fcf18ada890487e89b92f56cc37c747c6c9fef6c
# Parent  5819e85ad261928ba6deeca52d347481805c9583
Deleted a redundant pattern

diff -r 5819e85ad261 -r fcf18ada8904 src/Tools/rm-logfiles
--- a/src/Tools/rm-logfiles	Fri Nov 08 14:02:51 1996 +0100
+++ b/src/Tools/rm-logfiles	Fri Nov 08 14:04:38 1996 +0100
@@ -3,4 +3,4 @@
 #Remove useless files from subdirectories
 rm log */make*.log */make*.log.gz
 rm */test
-rm */.*.thy.ML */.*.thy.ML */*/.*.thy.ML
+rm */.*.thy.ML */*/.*.thy.ML