# HG changeset patch
# User wenzelm
# Date 1127747688 -7200
# Node ID 34c41d9bd749bef0ad03eac9ab4fff55519bc2d5
# Parent  b1ef33ebfa17870655fbc334ac955b8173e703f9
really copy doc/Contents;

diff -r b1ef33ebfa17 -r 34c41d9bd749 Admin/makedist
--- a/Admin/makedist	Mon Sep 26 16:10:19 2005 +0200
+++ b/Admin/makedist	Mon Sep 26 17:14:48 2005 +0200
@@ -227,7 +227,7 @@
 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
 gzip "${DISTNAME}_pdf.tar"
 
-mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
+mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc/Contents" "$DISTNAME/doc"
 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf