mirror of https://gerrit.osmocom.org/osmo-ci
jobs/coverity.yml: add parameter for git branch
Allow configuring a different git branch before starting the build. This is especially useful to reproduce a failure that only happens when using coverity tools during a build. Change-Id: I5f7c615ff5af4bf1f34ccef62767b5ca71cd2d8d
This commit is contained in:
parent
ff94d1def5
commit
e1540eee9e
|
@ -24,13 +24,18 @@
|
||||||
- build-discarder:
|
- build-discarder:
|
||||||
days-to-keep: 30
|
days-to-keep: 30
|
||||||
num-to-keep: 30
|
num-to-keep: 30
|
||||||
|
parameters:
|
||||||
|
- string:
|
||||||
|
name: BRANCH
|
||||||
|
description: osmo-ci.git branch
|
||||||
|
default: 'origin/master'
|
||||||
scm:
|
scm:
|
||||||
- git:
|
- git:
|
||||||
url: git://git.osmocom.org/osmo-ci
|
url: git://git.osmocom.org/osmo-ci
|
||||||
git-config-name: 'Jenkins Builder'
|
git-config-name: 'Jenkins Builder'
|
||||||
git-config-email: 'jenkins@osmocom.org'
|
git-config-email: 'jenkins@osmocom.org'
|
||||||
branches:
|
branches:
|
||||||
- 'origin/master'
|
- '$BRANCH'
|
||||||
triggers:
|
triggers:
|
||||||
- timed: "@daily"
|
- timed: "@daily"
|
||||||
publishers:
|
publishers:
|
||||||
|
|
Loading…
Reference in New Issue