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