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)