diff --git a/make-dist b/make-dist index 06cb8320af6..5aa1c17ca5e 100755 --- a/make-dist +++ b/make-dist @@ -74,6 +74,28 @@ while [ $# -gt 0 ]; do "--compress") default_gzip="compress" ;; + + "--snapshot") + clean_up=yes + make_tar=yes + update=no + check=no + ;; + + "--help") + echo "Usage: ${progname} [options]" + echo "" + echo " --clean-up delete staging directories when done" + echo " --compress use compress 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" + echo " --snapshot same as --clean-up --no-update --tar --no-check" + echo " --tar make a tar file" + echo "" + exit 0 + ;; + * ) echo "${progname}: Unrecognized argument: $1" >&2 exit 1