find -print;
authorwenzelm
Wed, 02 Jun 1999 11:55:18 +0200
changeset 6758 8fc15183f549
parent 6757 604d1445c9f3
child 6759 8ce58492bf50
find -print;
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