changeset 6750 | 0681dd2211b5 |
parent 6748 | f1f70344b749 |
child 6758 | 8fc15183f549 |
1.1 --- a/Admin/makedist Fri May 28 18:00:53 1999 +0200 1.2 +++ b/Admin/makedist Fri May 28 18:20:58 1999 +0200 1.3 @@ -177,6 +177,9 @@ 1.4 $TAR cf $DISTNAME.tar $DISTNAME 1.5 ( cd pdf; $TAR cf ../${DISTNAME}_pdf.tar $DISTNAME; ) 1.6 1.7 +mv pdf/$DISTNAME/doc/*.pdf $DISTNAME/doc 1.8 +rmdir pdf/$DISTNAME/doc pdf/$DISTNAME 1.9 + 1.10 UNPACKED_SIZE=$[ $(cat $DISTNAME.tar ${DISTNAME}_pdf.tar | wc -c) / 1024 ] 1.11 1.12 gzip $DISTNAME.tar