diff -r 50be659d4222 -r dd25f5f9641a Admin/makedist
--- a/Admin/makedist	Fri Oct 06 17:35:58 2000 +0200
+++ b/Admin/makedist	Sun Oct 08 19:58:26 2000 +0200
@@ -49,7 +49,7 @@
   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 Isabelle99-XX isabelle
+        cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle99-X isabelle
       PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
 EOF
   fi