Admin/makedist
changeset 5769 6a422b22ba02
parent 5727 1b708bfb0c1e
child 5817 02f4ff005a78
--- a/Admin/makedist	Sat Oct 24 21:25:43 1998 +0200
+++ b/Admin/makedist	Sun Oct 25 12:33:27 1998 +0100
@@ -32,8 +32,7 @@
   Checklist for official releases (before running this script):
 
     * Check that README files are up to date (should have Id: lines).
-    * Check that Pure/ROOT.ML/version is up to date!
-    * Check release name and date in NEWS!
+    * Check Admin/index.html.
     * Make sure that encoding info is consistent (fixencoding)!
     * Make sure that the repository version of Doc is consistent
       (watch out for *.bbl, *.rao, *.ind)!