# HG changeset patch
# User lcp
# Date 788013362 -3600
# Node ID 11e4827b3d75251ba97334df27d9e623688c0fca
# Parent  8928f1c44d80e21d24898c0b80c351f76407a6c4
Id: marker.

diff -r 8928f1c44d80 -r 11e4827b3d75 src/Tools/make-all
--- 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
diff -r 8928f1c44d80 -r 11e4827b3d75 src/Tools/rm-logfiles
--- 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 {} \;