Admin/makedist

--- a/Admin/makedist	Wed Oct 07 13:21:50 1998 +0200
+++ b/Admin/makedist	Wed Oct 07 17:51:11 1998 +0200
@@ -104,6 +104,7 @@
 
 export CVSROOT
 cvs -f -q $EXPORT -d $DISTNAME isabelle
+find . -name CVS -exec rm -rf {} \;
 
 
 # make docs
@@ -122,8 +123,6 @@
 
 cd $DISTBASE/$DISTNAME
 
-find . -name CVS -exec rm -rf {} \;
-
 find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) \) \
   -exec mv -f {} Distribution/doc \;
 rm Distribution/doc/Isa-logics.eps