# HG changeset patch # User wenzelm # Date 1212928149 -7200 # Node ID 2f45c1b1b05dbfd0e3600b4dbab6036bcf8589f7 # Parent 480f19078b6542e9d1c6fdf4c79f6cb42dd491a3 remove codegen_process.pdf from distribution; diff -r 480f19078b65 -r 2f45c1b1b05d Admin/makedist --- a/Admin/makedist Sat Jun 07 19:18:38 2008 +0200 +++ b/Admin/makedist Sun Jun 08 14:29:09 2008 +0200 @@ -180,6 +180,7 @@ 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 Distribution/doc/codegen_process.pdf rm -rf Doc mkdir src contrib