Merge branch 'master' into dwarf

1 files changed, 2 insertions, 2 deletions

diff --git a/configure b/configure
index b680ce3d..60ea1be7 100755
--- a/configure
+++ b/configure
@@ -65,9 +65,9 @@ while : ; do
     -toolprefix|--toolprefix)
         toolprefix="$2"; shift;;
     -no-runtime-lib)
-        has_runtime_lib=false; shift;;
+        has_runtime_lib=false;;
     -no-checklink)
-        build_checklink=false; shift;;
+        build_checklink=false;;
     *)
         if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
         target="$1";;