diff options
| author | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2016-07-01 17:23:35 +0100 |
|---|---|---|
| committer | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2016-07-01 17:23:35 +0100 |
| commit | 5f97f95b6ddd8e5dc1d5e6f94e1492b78cf3389c (patch) | |
| tree | ade44cf9289c4c0258714afea7a35d3f7fec3716 /MakeRelease.job | |
| parent | 1d5fd59b1a53160d79e62a7a3a67ee5aa9f94cf7 (diff) | |
MakeRelease.job: Fix the option name.
It is expected that jenkins UI sets "extra" parameter to either nothing,
or "--extra ../config/gcc6" or "--extra ../config/gcc5".
Change-Id: I4f3a022b52d5dddd29d17542a4237ee41272f289
Diffstat (limited to 'MakeRelease.job')
| -rwxr-xr-x | MakeRelease.job | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/MakeRelease.job b/MakeRelease.job index 89e7985a..e8c58db8 100755 --- a/MakeRelease.job +++ b/MakeRelease.job @@ -63,7 +63,7 @@ fi update="" if test x"${extra}" != x; then - extra="--extraconfig ${extra}" + extra="--extraconfigdir ${extra}" fi if test x"${runtests}" = xtrue; then |