# HG changeset patch
# User wenzelm
# Date 1127306755 -7200
# Node ID bde06ed41123618cd0dd2593f992d2541d55394a
# Parent  b4b8858580363b7644a9622d678a07160bf6b6ad
fixed cvs export;

diff -r b4b885858036 -r bde06ed41123 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