* make-dist: Add options for xz compression and no compression.

This commit is contained in:
Glenn Morris 2013-01-09 20:00:02 -08:00
parent 5062005180
commit 39aff4a79f
2 changed files with 14 additions and 0 deletions

View file

@ -1,3 +1,7 @@
2013-01-10 Glenn Morris <rgm@gnu.org>
* make-dist: Add options for xz compression and no compression.
2013-01-04 Glenn Morris <rgm@gnu.org>
* info/dir: Add htmlfontify.

View file

@ -87,6 +87,13 @@ while [ $# -gt 0 ]; do
"--lzma")
default_gzip="lzma"
;;
## Same with xz.
"--xz")
default_gzip="xz"
;;
"--no-compress")
default_gzip="cat"
;;
"--snapshot")
clean_up=yes
@ -101,6 +108,8 @@ while [ $# -gt 0 ]; do
echo " --bzip2 use bzip2 instead of gzip"
echo " --clean-up delete staging directories when done"
echo " --lzma use lzma instead of gzip"
echo " --xz use xz instead of gzip"
echo " --no-compress don't compress"
echo " --newer=TIME don't include files older than TIME"
echo " --no-check don't check for bad file names etc."
echo " --no-update don't recompile or do analogous things"
@ -510,6 +519,7 @@ if [ "${make_tar}" = yes ]; then
case "${default_gzip}" in
bzip2) gzip_extension=.bz2 ;;
lzma) gzip_extension=.lzma ;;
xz) gzip_extension=.xz ;;
gzip) gzip_extension=.gz ; default_gzip="gzip --best";;
*) gzip_extension= ;;
esac