diff options
-rwxr-xr-x | scripts/config | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/scripts/config b/scripts/config index ee355394f4ef..bb4d3deb6d1c 100755 --- a/scripts/config +++ b/scripts/config | |||
@@ -101,7 +101,6 @@ while [ "$1" != "" ] ; do | |||
101 | case "$CMD" in | 101 | case "$CMD" in |
102 | --keep-case|-k) | 102 | --keep-case|-k) |
103 | MUNGE_CASE=no | 103 | MUNGE_CASE=no |
104 | shift | ||
105 | continue | 104 | continue |
106 | ;; | 105 | ;; |
107 | --refresh) | 106 | --refresh) |