equal
deleted
inserted
replaced
85 if [ "$VERSION" = "-" ]; then |
85 if [ "$VERSION" = "-" ]; then |
86 DISTIDENT="Isabelle_$DATE" |
86 DISTIDENT="Isabelle_$DATE" |
87 [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" |
87 [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" |
88 DISTVERSION="$DISTNAME" |
88 DISTVERSION="$DISTNAME" |
89 EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" |
89 EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" |
90 UNOFFICIAL="unofficial" |
90 UNOFFICIAL=true |
91 else |
91 else |
92 DISTIDENT="$VERSION" |
92 DISTIDENT="$VERSION" |
93 [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" |
93 [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" |
94 DISTVERSION="$DISTNAME: $DISTDATE" |
94 DISTVERSION="$DISTNAME: $DISTDATE" |
95 EXPORT="cvs -f -q export -P -r $VERSION -d $DISTNAME isabelle" |
95 EXPORT="cvs -f -q export -P -r $VERSION -d $DISTNAME isabelle" |