# HG changeset patch
# User wenzelm
# Date 864312287 -7200
# Node ID d8114e93ef66dc4929ee3dc6b6a772a19f7a72f5
# Parent  08952002358dbd4ef5985de1ef53c3b431dc5ccb
fixed doc;

diff -r 08952002358d -r d8114e93ef66 Admin/makedist
--- a/Admin/makedist	Thu May 22 16:37:00 1997 +0200
+++ b/Admin/makedist	Thu May 22 16:44:47 1997 +0200
@@ -122,7 +122,8 @@
 find . -name CVS -exec rm -rf {} \;
 
 mkdir -p Tools/8bit/bin    #FIXME tmp
-find Doc -name \*.dvi -o -name \*.eps -o -name \*.ps -exec mv {} Distribution/doc \;
+find Doc \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) -exec mv {} Distribution/doc \;
+rm Distribution/doc/Isa-logics.eps
 rm -rf Admin Doc
 
 mkdir src