# HG changeset patch
# User wenzelm
# Date 884282673 -3600
# Node ID e723ce456305a83505a4667a172d1e188ea6eae7
# Parent  36ef28482123cf6902ba6ac1fc9cea4e110614cd
tuned;

diff -r 36ef28482123 -r e723ce456305 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