1.1 --- a/Admin/makedist	Tue Jul 21 16:43:38 1998 +0200
     1.2 +++ b/Admin/makedist	Tue Jul 21 17:30:13 1998 +0200
     1.3 @@ -124,7 +124,8 @@
     1.4  
     1.5  find . -name CVS -exec rm -rf {} \;
     1.6  
     1.7 -find Doc \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) -exec mv {} Distribution/doc \;
     1.8 +find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) \) \
     1.9 +  -exec mv -f {} Distribution/doc \;
    1.10  rm Distribution/doc/Isa-logics.eps
    1.11  cp Admin/index.html $DISTBASE
    1.12  rm -rf Admin Doc