Admin/makedist

--- 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