equal
deleted
inserted
replaced
33 Checklist for official releases (before running this script): |
33 Checklist for official releases (before running this script): |
34 |
34 |
35 * Check that README files are up to date (should have Id: lines). |
35 * Check that README files are up to date (should have Id: lines). |
36 * Check that Pure/ROOT.ML/version is up to date! |
36 * Check that Pure/ROOT.ML/version is up to date! |
37 * Check release name and date in NEWS! |
37 * Check release name and date in NEWS! |
|
38 * Make sure that encoding info is consistent (fixencoding)! |
38 * Make sure that the repository version of Doc is consistent |
39 * Make sure that the repository version of Doc is consistent |
39 (watch out for *.bbl, *.rao, *.ind)! |
40 (watch out for *.bbl, *.rao, *.ind)! |
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 |