Admin/makedist

--- a/Admin/makedist	Thu Jan 08 18:28:03 1998 +0100
+++ b/Admin/makedist	Thu Jan 08 19:04:33 1998 +0100
@@ -43,7 +43,7 @@
   if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then
     cat <<EOF
     * Tag the current repository version, e.g.:
-        cvs rtag Isabelle94-XX isabelle
+        cvs -d $CVSROOT rtag Isabelle94-XX isabelle
       PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
 EOF
   fi