--- 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"