# HG changeset patch
# User wenzelm
# Date 939836673 -7200
# Node ID c67eb6ed6a874e5a13a22cce70868390a7fc9a6e
# Parent  2cd88d1eec0c1956791b1387947d8608b8113fe5
berghofe;

diff -r 2cd88d1eec0c -r c67eb6ed6a87 Admin/makedist
--- a/Admin/makedist	Wed Oct 13 19:44:15 1999 +0200
+++ b/Admin/makedist	Wed Oct 13 19:44:33 1999 +0200
@@ -35,12 +35,10 @@
     * Check that README files are up to date (should have Id: lines).
     * 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)!
     * Check ML_SYSTEM defaults!
 EOF
   #Wicked! We just won't tell other users ...
-  if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then
+  if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm -o $LOGNAME = berghofe ]; then
     cat <<EOF
     * Tag the current repository version, e.g.:
         cvs -d $CVSROOT rtag Isabelle94-XX isabelle