author | wenzelm |
Thu, 08 Jan 1998 19:04:33 +0100 | |
changeset 4542 | e723ce456305 |
parent 4541 | 36ef28482123 |
child 4543 | 82a45bdd0e80 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- 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