1.1 --- a/Admin/makedist	Wed Oct 07 13:21:50 1998 +0200
     1.2 +++ b/Admin/makedist	Wed Oct 07 17:51:11 1998 +0200
     1.3 @@ -104,6 +104,7 @@
     1.4  
     1.5  export CVSROOT
     1.6  cvs -f -q $EXPORT -d $DISTNAME isabelle
     1.7 +find . -name CVS -exec rm -rf {} \;
     1.8  
     1.9  
    1.10  # make docs
    1.11 @@ -122,8 +123,6 @@
    1.12  
    1.13  cd $DISTBASE/$DISTNAME
    1.14  
    1.15 -find . -name CVS -exec rm -rf {} \;
    1.16 -
    1.17  find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) \) \
    1.18    -exec mv -f {} Distribution/doc \;
    1.19  rm Distribution/doc/Isa-logics.eps