Admin/makedist
changeset 3363 8557c2a1750c
parent 3305 d8114e93ef66
child 3638 2b67561c6488
--- 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