# HG changeset patch
# User wenzelm
# Date 863628108 -7200
# Node ID 57be77ca36ff8d8752a9d8a1d8da784152f5e065
# Parent  7a6c933d51d0b4c4023ff9a1815719cfa6b03599
tuned comment;

diff -r 7a6c933d51d0 -r 57be77ca36ff 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