author | wenzelm |
Wed, 14 May 1997 18:41:48 +0200 | |
changeset 3186 | 57be77ca36ff |
parent 3185 | 7a6c933d51d0 |
child 3187 | 8f8c88dcd728 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- 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