Admin/makedist
changeset 16328 49c1f9dedc56
parent 16301 f9f2e1643593
child 16481 fe61cdf5af51
--- a/Admin/makedist	Thu Jun 09 11:04:02 2005 +0200
+++ b/Admin/makedist	Thu Jun 09 11:04:54 2005 +0200
@@ -53,7 +53,7 @@
   Checklist for official releases (before running this script):
 
     * Check Admin/page contents.
-    * Check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT.
+    * Check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
     * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
     * Tag the current repository version, e.g.:
         cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle2002 isabelle
@@ -267,7 +267,9 @@
 mv "$DISTNAME" "${DISTNAME}-old"
 mkdir "$DISTNAME"
 
-mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "$DISTNAME"
+mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
+   "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
+   "$DISTNAME"
 mkdir "$DISTNAME/doc"
 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/index.html" "$DISTNAME/doc"