1.1 --- a/Admin/makedist	Wed Sep 21 14:23:57 2005 +0200
     1.2 +++ b/Admin/makedist	Wed Sep 21 14:45:55 2005 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4    DISTIDENT="$VERSION"
     1.5    [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
     1.6    DISTVERSION="$DISTNAME: $DISTDATE"
     1.7 -  EXPORT="cvs -f -q export -P -r $VERSION -d $DISTNAME isabelle"
     1.8 +  EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle"
     1.9    UNOFFICIAL=""
    1.10  fi
    1.11