jenkins.sh: Fix handling of --extraconfig opton.

Change-Id: I499c4ed5d2f1c872de200ac2072e0ba0eebcfcec

1 files changed, 1 insertions, 1 deletions

diff --git a/jenkins.sh b/jenkins.sh
index ac4d5a62..87b5c195 100755
--- a/jenkins.sh
+++ b/jenkins.sh
@@ -99,7 +99,7 @@ while test $# -gt 0; do
     case $1 in
 	--gcc-branch) change="$change gcc=$2"; shift ;;
 	--override) change="$change $2"; shift ;;
-	--extraconfig) change="${change} --extraconfig $2" ;;
+	--extraconfig) change="${change} --extraconfig $2"; shift ;;
         -s|--snapshots) user_snapshots=$2; shift ;;
         -g|--gitrepo) git_reference=$2; shift ;;
         --abedir) abe_dir=$2; shift ;;