fixed cvs export;
authorwenzelm
Wed, 21 Sep 2005 14:45:55 +0200
changeset 17561 bde06ed41123
parent 17560 b4b885858036
child 17562 623c9e8668aa
fixed cvs export;
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