# HG changeset patch
# User wenzelm
# Date 928317318 -7200
# Node ID 8fc15183f549da24e8e14e6b513aaecd8430df8a
# Parent  604d1445c9f3a63d2375279d8e730548a30faca2
find -print;

diff -r 604d1445c9f3 -r 8fc15183f549 Admin/makedist
--- a/Admin/makedist	Tue Jun 01 19:47:10 1999 +0200
+++ b/Admin/makedist	Wed Jun 02 11:55:18 1999 +0200
@@ -126,8 +126,7 @@
 
 cd $DISTBASE/$DISTNAME
 
-MOVE=$(find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) \) \
-  | grep -v 'gfx/.*pdf')
+MOVE=$(find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
 mv -f $MOVE Distribution/doc
 rm Distribution/doc/Isa-logics.eps
 cp Admin/index.html $DISTBASE