Admin/makedist
changeset 17653 34c41d9bd749
parent 17651 a6499b0c5a40
child 17655 0039abe88816
equal deleted inserted replaced
17652:b1ef33ebfa17 17653:34c41d9bd749
   225 
   225 
   226 echo "${DISTNAME}_pdf.tar.gz"
   226 echo "${DISTNAME}_pdf.tar.gz"
   227 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   227 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   228 gzip "${DISTNAME}_pdf.tar"
   228 gzip "${DISTNAME}_pdf.tar"
   229 
   229 
   230 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
   230 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc/Contents" "$DISTNAME/doc"
   231 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   231 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   232 
   232 
   233 
   233 
   234 # cleanup dist
   234 # cleanup dist
   235 
   235