diff --git a/[refs] b/[refs]
index a72fbe1b125d..f10a5ae58dd1 100644
--- a/[refs]
+++ b/[refs]
@@ -1,2 +1,2 @@
 ---
-refs/heads/master: 923e02ecf3f8db19d52176723fefa0ffe6e9a3cd
+refs/heads/master: c6ba8d06ecfc1dadcf7f1b54960cf9332ba5ae8d
diff --git a/trunk/scripts/config b/trunk/scripts/config
index ee355394f4ef..bb4d3deb6d1c 100755
--- a/trunk/scripts/config
+++ b/trunk/scripts/config
@@ -101,7 +101,6 @@ while [ "$1" != "" ] ; do
 	case "$CMD" in
 	--keep-case|-k)
 		MUNGE_CASE=no
-		shift
 		continue
 		;;
 	--refresh)