diff --git a/contrib/dist/make_dist_tarball b/contrib/dist/make_dist_tarball index 74ec93450a..5c2b625852 100755 --- a/contrib/dist/make_dist_tarball +++ b/contrib/dist/make_dist_tarball @@ -46,6 +46,7 @@ DISTCHECK_MAKE_FLAGS=-j4 # tarballs; but higher-than-expected versions are ok for # non-distribution tarballs. dirty_ok=0 +gnu_version_ignore=0 dist_target=distcheck distcheck_flags="AM_MAKEFLAGS=$DISTCHECK_MAKE_FLAGS" if test "`basename $0`" = "make_tarball"; then @@ -74,6 +75,8 @@ while test "$1" != ""; do -distdir) distdir=$2; shift ;; --distdir) distdir=$2; shift ;; --dirtyok) dirty_ok=1; shift ;; + --verok) gnu_version_ignore=1;; + -verok) gnu_version_ignore=1;; *) cat <