tuned;
authorwenzelm
Thu, 08 Jan 1998 19:04:33 +0100
changeset 4542 e723ce456305
parent 4541 36ef28482123
child 4543 82a45bdd0e80
tuned;
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