Admin/makedist
changeset 5817 02f4ff005a78
parent 5769 6a422b22ba02
child 6296 9da8f9262c4c
equal deleted inserted replaced
5816:6f3cb53502fa 5817:02f4ff005a78
    29   release to be exported from the repository, or "-" to checkout the
    29   release to be exported from the repository, or "-" to checkout the
    30   current sources as an unofficial release.
    30   current sources as an unofficial release.
    31 
    31 
    32   Checklist for official releases (before running this script):
    32   Checklist for official releases (before running this script):
    33 
    33 
       
    34     * Check release name and date in NEWS!
    34     * 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).
    35     * Check Admin/index.html.
    36     * Check Admin/index.html.
    36     * Make sure that encoding info is consistent (fixencoding)!
    37     * Make sure that encoding info is consistent (fixencoding)!
    37     * Make sure that the repository version of Doc is consistent
    38     * Make sure that the repository version of Doc is consistent
    38       (watch out for *.bbl, *.rao, *.ind)!
    39       (watch out for *.bbl, *.rao, *.ind)!