tuned comment;
authorwenzelm
Wed, 14 May 1997 18:41:48 +0200
changeset 3186 57be77ca36ff
parent 3185 7a6c933d51d0
child 3187 8f8c88dcd728
tuned comment;
Admin/makedist
--- a/Admin/makedist	Wed May 14 18:38:15 1997 +0200
+++ b/Admin/makedist	Wed May 14 18:41:48 1997 +0200
@@ -37,6 +37,7 @@
     * Make sure that encoding info is consistent (fixencoding)!
     * Make sure that the repository version of Doc is consistent
       (watch out for *.bbl, *.rao, *.ind)!
+    * Check ML_SYSTEM defaults!
 EOF
   #Wicked! We just won't tell other users ...
   if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then