--- a/Admin/makedist Wed Sep 27 19:37:32 2000 +0200
+++ b/Admin/makedist Wed Sep 27 19:39:50 2000 +0200
@@ -214,16 +214,17 @@
mkdir -p "pdf/$DISTNAME/doc"
mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
-echo "$DISTNAME.tar"
+echo "$DISTNAME.tar.gz"
"$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
+gzip "$DISTNAME.tar"
+
+echo "${DISTNAME}_pdf.tar.gz"
( cd pdf; echo "${DISTNAME}_pdf.tar"; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
+gzip "${DISTNAME}_pdf.tar"
mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
-echo "$DISTNAME.tar.gz" && gzip "$DISTNAME.tar"
-echo "${DISTNAME}_pdf.tar.gz" && gzip "${DISTNAME}_pdf.tar"
-
# cleanup dist