diff options
author | Miles Bader <miles@gnu.org> | 2008-01-30 07:57:28 +0000 |
---|---|---|
committer | Miles Bader <miles@gnu.org> | 2008-01-30 07:57:28 +0000 |
commit | d235ca2ff8fab139ce797757fcb159d1e28fa7e0 (patch) | |
tree | 96c5cd1a06a0d9dc26e8470c6eabfc032c0046f3 /make-dist | |
parent | 3709a060f679dba14df71ae64a0035fa2b5b3106 (diff) | |
parent | 02cbe062bee38a6705bafb1699d77e3c44cfafcf (diff) | |
download | emacs-d235ca2ff8fab139ce797757fcb159d1e28fa7e0.tar.gz |
Merge from emacs--devo--0
Revision: emacs@sv.gnu.org/emacs--unicode--0--patch-324
Diffstat (limited to 'make-dist')
-rwxr-xr-x | make-dist | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/make-dist b/make-dist index 9ab0388275f..0f632f24d89 100755 --- a/make-dist +++ b/make-dist @@ -85,6 +85,10 @@ while [ $# -gt 0 ]; do "--bzip2") default_gzip="bzip2" ;; + ## Same with lzma. + "--lzma") + default_gzip="lzma" + ;; "--snapshot") clean_up=yes @@ -96,9 +100,10 @@ while [ $# -gt 0 ]; do "--help") echo "Usage: ${progname} [options]" echo "" - echo " --bzip2 use bzip2 instead of gzip" + echo " --bzip2 use bzip2 instead of gzip" echo " --clean-up delete staging directories when done" echo " --compress use compress instead of gzip" + echo " --lzma use lzma instead of gzip" 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" @@ -750,6 +755,7 @@ if [ "${make_tar}" = yes ]; then case "${default_gzip}" in bzip2) gzip_extension=.bz2 ;; compress* ) gzip_extension=.Z ;; + lzma) gzip_extension=.lzma ;; * ) gzip_extension=.gz ;; esac echo "Creating tar file" |