Admin/makedist
changeset 10169 dd25f5f9641a
parent 10112 76d029a4c42e
child 10532 042f67eea015
equal deleted inserted replaced
10168:50be659d4222 10169:dd25f5f9641a
    47 EOF
    47 EOF
    48   #Wicked! We just won't tell other users ...
    48   #Wicked! We just won't tell other users ...
    49   if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm -o $LOGNAME = berghofe ]; then
    49   if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm -o $LOGNAME = berghofe ]; then
    50     cat <<EOF
    50     cat <<EOF
    51     * Tag the current repository version, e.g.:
    51     * Tag the current repository version, e.g.:
    52         cvs -d $CVSROOT rtag Isabelle99-XX isabelle
    52         cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle99-X isabelle
    53       PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
    53       PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
    54 EOF
    54 EOF
    55   fi
    55   fi
    56   cat <<EOF
    56   cat <<EOF
    57 
    57