# HG changeset patch
# User wenzelm
# Date 1127755152 -7200
# Node ID 0039abe8881665a035f1c5cd040c9f9340b4f8a7
# Parent  38496187809de819eeea069946635285b43f42c3
yet another atempt to get doc/Contents right;

diff -r 38496187809d -r 0039abe88816 Admin/makedist
--- a/Admin/makedist	Mon Sep 26 19:04:31 2005 +0200
+++ b/Admin/makedist	Mon Sep 26 19:19:12 2005 +0200
@@ -217,7 +217,9 @@
 chgrp -R isabelle "$DISTNAME" Isabelle
 
 mkdir -p "pdf/$DISTNAME/doc"
-mv "$DISTNAME/doc/"*.pdf "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc"
+mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
+
+sync; sleep 3
 
 echo "$DISTNAME.tar.gz"
 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
@@ -227,7 +229,7 @@
 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
 gzip "${DISTNAME}_pdf.tar"
 
-mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc/Contents" "$DISTNAME/doc"
+mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
 
 
@@ -240,7 +242,7 @@
   "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
   "$DISTNAME"
 mkdir "$DISTNAME/doc"
-mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc"
+mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
 
 chgrp -R isabelle "$DISTNAME"