Admin/makedist
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