diff --git a/scripts/config b/scripts/config index ee355394f4ef76eeb6d6f74dac00729d8cc942e3..bb4d3deb6d1c0add7815115a14a574212c0f3d90 100755 --- a/scripts/config +++ b/scripts/config @@ -101,7 +101,6 @@ while [ "$1" != "" ] ; do case "$CMD" in --keep-case|-k) MUNGE_CASE=no - shift continue ;; --refresh)