Id: marker.

--- a/src/Tools/make-all	Wed Dec 21 13:26:26 1994 +0100
+++ b/src/Tools/make-all	Wed Dec 21 13:36:02 1994 +0100
@@ -1,6 +1,6 @@
 #! /bin/sh
-#
-#make-all: make all systems afresh
+# $Id$
+#Make all systems afresh
 
 # Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
 # displays the last few lines of these files -- this indicates whether

--- a/src/Tools/rm-logfiles	Wed Dec 21 13:26:26 1994 +0100
+++ b/src/Tools/rm-logfiles	Wed Dec 21 13:36:02 1994 +0100
@@ -1,5 +1,6 @@
 #! /bin/sh
-#rm-logfiles: remove useless files from subdirectories
+# $Id$
+#Remove useless files from subdirectories
 rm log */make*.log */make*.log.gz
 rm */test
 find . -name '.*.thy.ML' -print -exec rm {} \;