# HG changeset patch
# User wenzelm
# Date 1127742988 -7200
# Node ID a6499b0c5a4056bbe8e8d96da270e017d0bfffca
# Parent  44b135d04cc4ae26057b5146a2fcce0957289c11
copy doc/Contents;

diff -r 44b135d04cc4 -r a6499b0c5a40 Admin/makedist
--- a/Admin/makedist	Mon Sep 26 15:17:33 2005 +0200
+++ b/Admin/makedist	Mon Sep 26 15:56:28 2005 +0200
@@ -217,7 +217,7 @@
 chgrp -R isabelle "$DISTNAME" Isabelle
 
 mkdir -p "pdf/$DISTNAME/doc"
-mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
+mv "$DISTNAME/doc/"*.pdf "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc"
 
 echo "$DISTNAME.tar.gz"
 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"