From ad2d788d6c0d831ea4aeebae12895e89e955c29a Mon Sep 17 00:00:00 2001 From: Ethan P Date: Fri, 29 Jul 2022 14:01:55 -0700 Subject: [PATCH] build: Add more '--no-*' options --- build.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/build.sh b/build.sh index 7b38b54..f6a459f 100755 --- a/build.sh +++ b/build.sh @@ -382,8 +382,11 @@ while shiftopt; do --compress) OPT_COMPRESS=true ;; --manuals) OPT_MANUALS="${OPT_VAL:-true}" ;; --no-manuals) OPT_MANUALS=false ;; + --verify) OPT_VERIFY=true ;; --no-verify) OPT_VERIFY=false ;; + --banner) OPT_BANNER=true ;; --no-banner) OPT_BANNER=false ;; + --inline) OPT_INLINE=true ;; --no-inline) OPT_INLINE=false ;; --prefix) shiftval; OPT_PREFIX="$OPT_VAL" ;; --alternate-executable) shiftval; OPT_BAT="$OPT_VAL" ;;