equal
deleted
inserted
replaced
217 echo "$DISTNAME.tar.gz" |
217 echo "$DISTNAME.tar.gz" |
218 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" |
218 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" |
219 gzip "$DISTNAME.tar" |
219 gzip "$DISTNAME.tar" |
220 |
220 |
221 echo "${DISTNAME}_pdf.tar.gz" |
221 echo "${DISTNAME}_pdf.tar.gz" |
222 ( cd pdf; echo "${DISTNAME}_pdf.tar"; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) |
222 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) |
223 gzip "${DISTNAME}_pdf.tar" |
223 gzip "${DISTNAME}_pdf.tar" |
224 |
224 |
225 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" |
225 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" |
226 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf |
226 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf |
227 |
227 |
241 |
241 |
242 |
242 |
243 # final note |
243 # final note |
244 |
244 |
245 echo "###" |
245 echo "###" |
246 echo "### Finished." |
246 echo "### Finished makedist." |
247 echo "###" |
247 echo "###" |