author | wenzelm |
Wed, 21 Sep 2005 14:45:55 +0200 | |
changeset 17561 | bde06ed41123 |
parent 17560 | b4b885858036 |
child 17562 | 623c9e8668aa |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Wed Sep 21 14:23:57 2005 +0200 +++ b/Admin/makedist Wed Sep 21 14:45:55 2005 +0200 @@ -92,7 +92,7 @@ DISTIDENT="$VERSION" [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" DISTVERSION="$DISTNAME: $DISTDATE" - EXPORT="cvs -f -q export -P -r $VERSION -d $DISTNAME isabelle" + EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle" UNOFFICIAL="" fi