# HG changeset patch # User wenzelm # Date 901035013 -7200 # Node ID 0af867c248ee07d1cd1a8e3620551d045f2c0e56 # Parent cca9a908c27090152bbbffb6e976f85c48a75a58 fixed eps/ps find; diff -r cca9a908c270 -r 0af867c248ee Admin/makedist --- a/Admin/makedist Tue Jul 21 16:43:38 1998 +0200 +++ b/Admin/makedist Tue Jul 21 17:30:13 1998 +0200 @@ -124,7 +124,8 @@ find . -name CVS -exec rm -rf {} \; -find Doc \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) -exec mv {} Distribution/doc \; +find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) \) \ + -exec mv -f {} Distribution/doc \; rm Distribution/doc/Isa-logics.eps cp Admin/index.html $DISTBASE rm -rf Admin Doc