1.1 --- a/Admin/makedist	Wed Sep 27 19:37:32 2000 +0200
     1.2 +++ b/Admin/makedist	Wed Sep 27 19:39:50 2000 +0200
     1.3 @@ -214,16 +214,17 @@
     1.4  mkdir -p "pdf/$DISTNAME/doc"
     1.5  mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
     1.6  
     1.7 -echo "$DISTNAME.tar"
     1.8 +echo "$DISTNAME.tar.gz"
     1.9  "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
    1.10 +gzip "$DISTNAME.tar"
    1.11 +
    1.12 +echo "${DISTNAME}_pdf.tar.gz"
    1.13  ( cd pdf; echo "${DISTNAME}_pdf.tar"; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
    1.14 +gzip "${DISTNAME}_pdf.tar"
    1.15  
    1.16  mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
    1.17  rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
    1.18  
    1.19 -echo "$DISTNAME.tar.gz" && gzip "$DISTNAME.tar"
    1.20 -echo "${DISTNAME}_pdf.tar.gz" && gzip "${DISTNAME}_pdf.tar"
    1.21 -
    1.22  
    1.23  # cleanup dist
    1.24