# HG changeset patch
# User wenzelm
# Date 864743486 -7200
# Node ID 8557c2a1750c2dcdeca9d6fd7ed4f5a8c5ba9a57
# Parent  0b268cff9344268b18ab5241b5c45e3374f107cd
fixed -P (checkout only);

diff -r 0b268cff9344 -r 8557c2a1750c Admin/makedist
--- a/Admin/makedist	Tue May 27 15:45:07 1997 +0200
+++ b/Admin/makedist	Tue May 27 16:31:26 1997 +0200
@@ -79,7 +79,7 @@
 
 if [ "$VERSION" = "-" ]; then
   DISTNAME=Isabelle_$DATE
-  EXPORT="checkout"
+  EXPORT="checkout -P"
   UNOFFICIAL=true
 else
   DISTNAME="$VERSION"
@@ -100,7 +100,7 @@
 cd $DISTBASE
 
 export CVSROOT
-cvs -f -q $EXPORT -P -d $DISTNAME isabelle
+cvs -f -q $EXPORT -d $DISTNAME isabelle
 
 
 # make docs