diff -r 024b242bc26f -r d45f0af592f0 rm-logfiles
--- a/rm-logfiles	Thu Feb 03 16:06:55 1994 +0100
+++ b/rm-logfiles	Thu Feb 03 17:16:40 1994 +0100
@@ -1,6 +1,6 @@
 #! /bin/sh
 #rm-logfiles: remove useless files from subdirectories
-rm log */make*.log */make*.log.gz */make*.log.z
+rm log */make*.log */make*.log.gz
 rm */test
 rm */.*.thy.ML
 rm */ex/.*.thy.ML