diff options
| -rwxr-xr-x | autogen.sh | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/autogen.sh b/autogen.sh index fa8d2916ad..1897e23b53 100755 --- a/autogen.sh +++ b/autogen.sh @@ -19,13 +19,11 @@ set -e verb="$1" -if [[ -n "$verb" ]]; then - if [[ "$verb" != [cgals] ]]; then - echo "Unexpected argument: $verb" >&2 - exit 1 - fi - shift -fi +case "$verb" in +"") ;; +[cgals]) shift ;; +*) echo "Unexpected argument: $verb" >&2; exit 1 ;; +esac oldpwd=$(pwd) topdir=$(dirname $0) |