# HG changeset patch
# User wenzelm
# Date 1180628206 -7200
# Node ID b7d0e78be86d595dc12e6e4b3133b05211170dcb
# Parent  792ff2490f91f708bb3f0b10925ba32a1bfcee93
doc: exclude isabelle_isar.pdf;

diff -r 792ff2490f91 -r b7d0e78be86d Admin/makedist
--- a/Admin/makedist	Thu May 31 15:23:35 2007 +0200
+++ b/Admin/makedist	Thu May 31 18:16:46 2007 +0200
@@ -162,7 +162,7 @@
 DISTBASE=$DISTBASE
 EOF
 
-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')
+MOVE=$($FIND Doc \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -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