rmdir pdf;
authorwenzelm
Fri, 09 Jul 1999 19:11:50 +0200
changeset 69582ed4b761d6d5
parent 6957 d8026ebe4516
child 6959 d33b1629eaf9
rmdir pdf;
Admin/makedist
     1.1 --- a/Admin/makedist	Fri Jul 09 18:59:01 1999 +0200
     1.2 +++ b/Admin/makedist	Fri Jul 09 19:11:50 1999 +0200
     1.3 @@ -177,7 +177,7 @@
     1.4  ( cd pdf; $TAR cf ../${DISTNAME}_pdf.tar $DISTNAME; )
     1.5  
     1.6  mv pdf/$DISTNAME/doc/*.pdf $DISTNAME/doc
     1.7 -rmdir pdf/$DISTNAME/doc pdf/$DISTNAME
     1.8 +rmdir pdf/$DISTNAME/doc pdf/$DISTNAME pdf
     1.9  
    1.10  UNPACKED_SIZE=$[ $(cat $DISTNAME.tar ${DISTNAME}_pdf.tar | wc -c) / 1024 ]
    1.11