1.1 --- a/Admin/makedist	Mon Jun 20 21:34:31 2005 +0200
     1.2 +++ b/Admin/makedist	Mon Jun 20 22:13:53 2005 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  DISTNAME=$DISTNAME
     1.5  EOF
     1.6  
     1.7 -MOVE=$($FIND Doc \( -type f -a -not -type l -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
     1.8 +MOVE=$($FIND Doc \( -type f -a -not -type l -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
     1.9  mv -f $MOVE Distribution/doc
    1.10  rm Distribution/doc/Isa-logics.eps
    1.11  rm -rf Doc Tools