diff -r 2ce69d6d5581 -r af5221147455 Admin/makedist
--- a/Admin/makedist	Sun Jun 28 18:47:22 2009 +0200
+++ b/Admin/makedist	Sun Jun 28 19:29:28 2009 +0200
@@ -116,7 +116,6 @@
 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
 mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
-[ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
 
 cd "$DISTBASE"
 mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
@@ -141,7 +140,7 @@
 MOVE=$(find doc-src \( -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 doc
 rm doc/Isa-logics.eps
-rm doc/adaption.dvi doc/adaption.pdf doc/architecture.dvi doc/architecture.pdf
+rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
 rm -rf doc-src
 
 mkdir -p contrib
@@ -189,18 +188,9 @@
 chmod -R g=o "$DISTNAME"
 chgrp -R isabelle "$DISTNAME" Isabelle
 
-mkdir -p "pdf/$DISTNAME/doc"
-mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
-
 echo "$DISTNAME.tar.gz"
 tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
 
-echo "${DISTNAME}_pdf.tar.gz"
-tar -C pdf -czf "${DISTNAME}_pdf.tar.gz" "$DISTNAME"
-
-mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
-rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
-
 
 # cleanup dist