1.1 --- a/Admin/makedist	Fri May 28 17:59:22 1999 +0200
     1.2 +++ b/Admin/makedist	Fri May 28 18:00:33 1999 +0200
     1.3 @@ -92,6 +92,7 @@
     1.4  
     1.5  mkdir -p $DISTBASE || fail "Unable to create distribution base dir $DISTBASE!"
     1.6  [ -e $DISTBASE/$DISTNAME ] && fail "$DISTBASE/$DISTNAME already exists!"
     1.7 +[ -e $DISTBASE/pdf/$DISTNAME ] && fail "$DISTBASE/pdf/$DISTNAME already exists!"
     1.8  
     1.9  
    1.10  # export from repository
    1.11 @@ -167,18 +168,22 @@
    1.12  chown -R $LOGNAME:isabelle $DISTNAME
    1.13  chmod -R u+w $DISTNAME
    1.14  
    1.15 -if type -path gtar
    1.16 -then
    1.17 -  gtar cf $DISTNAME.tar $DISTNAME
    1.18 -else
    1.19 -  tar cf $DISTNAME.tar $DISTNAME
    1.20 -fi
    1.21 +TAR=tar
    1.22 +type -path gtar >/dev/null && TAR=gtar
    1.23  
    1.24 -UNPACKED_SIZE=$[ $(wc -c <$DISTNAME.tar) / 1024 ]
    1.25 +mkdir -p pdf/$DISTNAME/doc
    1.26 +mv $DISTNAME/doc/*.pdf pdf/$DISTNAME/doc
    1.27 +
    1.28 +$TAR cf $DISTNAME.tar $DISTNAME
    1.29 +( cd pdf; $TAR cf ../${DISTNAME}_pdf.tar $DISTNAME; )
    1.30 +
    1.31 +UNPACKED_SIZE=$[ $(cat $DISTNAME.tar ${DISTNAME}_pdf.tar | wc -c) / 1024 ]
    1.32  
    1.33  gzip $DISTNAME.tar
    1.34 +gzip ${DISTNAME}_pdf.tar
    1.35  
    1.36  PACKED_SIZE=$[ $(wc -c <$DISTNAME.tar.gz) / 1024 ]
    1.37 +PACKED_SIZE_PDF=$[ $(wc -c <${DISTNAME}_pdf.tar.gz) / 1024 ]
    1.38  
    1.39  
    1.40  # prepare dist index.html
    1.41 @@ -186,6 +191,7 @@
    1.42  perl -pi -e \
    1.43   "s/{ISABELLE}/$DISTNAME/g; \
    1.44    s/{PACKED_SIZE}/$PACKED_SIZE/g; \
    1.45 +  s/{PACKED_SIZE_PDF}/$PACKED_SIZE_PDF/g; \
    1.46    s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \
    1.47    s/{AUTHOR}/$LOGNAME/g; \
    1.48    s/{DATE}/$DATE/g;" \