changeset 17558 | de236aeb867c |
parent 17554 | d16abc8f4fb0 |
child 17560 | b4b885858036 |
--- a/Admin/makedist Wed Sep 21 14:02:57 2005 +0200 +++ b/Admin/makedist Wed Sep 21 14:03:30 2005 +0200 @@ -87,7 +87,7 @@ [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" DISTVERSION="$DISTNAME" EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" - UNOFFICIAL="unofficial" + UNOFFICIAL=true else DISTIDENT="$VERSION" [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"