author | wenzelm |
Tue, 27 May 1997 16:31:26 +0200 | |
changeset 3363 | 8557c2a1750c |
parent 3362 | 0b268cff9344 |
child 3364 | 8f225296fade |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- 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