diff -r abf475cf11f2 -r fe61cdf5af51 Admin/makedist
--- a/Admin/makedist	Mon Jun 20 21:34:31 2005 +0200
+++ b/Admin/makedist	Mon Jun 20 22:13:53 2005 +0200
@@ -176,7 +176,7 @@
 DISTNAME=$DISTNAME
 EOF
 
-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')
+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')
 mv -f $MOVE Distribution/doc
 rm Distribution/doc/Isa-logics.eps
 rm -rf Doc Tools