diff options
author | Christophe Lyon <christophe.lyon@linaro.org> | 2016-03-09 14:34:28 +0100 |
---|---|---|
committer | Christophe Lyon <christophe.lyon@linaro.org> | 2016-03-29 10:58:16 +0200 |
commit | 34b4e7622c79f8a7125e5ed565b45ca54d0f01ee (patch) | |
tree | 7d251f274101f235ede5100b066f713c934fd8eb /jenkins.sh | |
parent | 2b252f2a3df0fca9cfa008ec97869cb44f951111 (diff) |
Add support for --extraconfig <tool>=<path> option.
Change-Id: Iad2016cb3692c9320555a982311d5792b1a95ac0
Diffstat (limited to 'jenkins.sh')
-rwxr-xr-x | jenkins.sh | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -94,11 +94,12 @@ rebuild=true orig_parameters="$@" -OPTS="`getopt -o s:g:c:w:o:f:l:rt:b:h -l override:,gcc-branch:,snapshots:,gitrepo:,abe:,workspace:,options:,fileserver:,logserver:,logname:,languages:,runtests,target:,bootstrap,help,excludecheck:,norebuild -- "$@"`" +OPTS="`getopt -o s:g:c:w:o:f:l:rt:b:h -l override:,gcc-branch:,snapshots:,gitrepo:,abe:,workspace:,options:,fileserver:,logserver:,logname:,languages:,runtests,target:,bootstrap,help,excludecheck:,norebuild,extraconfig: -- "$@"`" 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" ;; -s|--snapshots) user_snapshots=$2; shift ;; -g|--gitrepo) git_reference=$2; shift ;; -c|--abe) abe_dir=$2; shift ;; |