equal
deleted
inserted
replaced
35 * Check that Pure/ROOT.ML/version is up to date! |
35 * Check that Pure/ROOT.ML/version is up to date! |
36 * Check release name and date in NEWS! |
36 * Check release name and date in NEWS! |
37 * Make sure that encoding info is consistent (fixencoding)! |
37 * Make sure that encoding info is consistent (fixencoding)! |
38 * Make sure that the repository version of Doc is consistent |
38 * Make sure that the repository version of Doc is consistent |
39 (watch out for *.bbl, *.rao, *.ind)! |
39 (watch out for *.bbl, *.rao, *.ind)! |
|
40 * Check ML_SYSTEM defaults! |
40 EOF |
41 EOF |
41 #Wicked! We just won't tell other users ... |
42 #Wicked! We just won't tell other users ... |
42 if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then |
43 if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then |
43 cat <<EOF |
44 cat <<EOF |
44 * Tag the current repository version, e.g.: |
45 * Tag the current repository version, e.g.: |