# HG changeset patch
# User wenzelm
# Date 907775471 -7200
# Node ID 5b56804edf85c90383cc7900387b67f895c8b359
# Parent  1fe18aca1062a548441f41e9b96ff557999faf4a
tuned rm CVS;

diff -r 1fe18aca1062 -r 5b56804edf85 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