equal
deleted
inserted
replaced
41 EOF |
41 EOF |
42 #Wicked! We just won't tell other users ... |
42 #Wicked! We just won't tell other users ... |
43 if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then |
43 if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then |
44 cat <<EOF |
44 cat <<EOF |
45 * Tag the current repository version, e.g.: |
45 * Tag the current repository version, e.g.: |
46 cvs rtag Isabelle94-XX isabelle |
46 cvs -d $CVSROOT rtag Isabelle94-XX isabelle |
47 PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING! |
47 PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING! |
48 EOF |
48 EOF |
49 fi |
49 fi |
50 cat <<EOF |
50 cat <<EOF |
51 |
51 |