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

2 files changed, 14 insertions, 0 deletions

diff --git a/ChangeLog b/ChangeLog
index 0dcbc4747fb..05d15b7dc36 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -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.
diff --git a/make-dist b/make-dist
index 60afb0c618f..788dca3462c 100755
--- a/make-dist
+++ b/make-dist
@@ -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