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