| changeset 820 | 11e4827b3d75 |
| parent 262 | 024b242bc26f |
| child 1146 | 75caf28a3aa9 |
--- 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