# 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