author | wenzelm |
Wed, 21 Sep 2005 14:03:30 +0200 | |
changeset 17558 | de236aeb867c |
parent 17557 | cbfd12c61a1f |
child 17559 | 70b4a2885193 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- 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"