diff options
author | 2019-09-03 17:08:42 +0000 | |
---|---|---|
committer | 2019-09-03 17:08:42 +0000 | |
commit | e39fa8b213ed7fe607298a66c93329663958de8a (patch) | |
tree | 7d9f503c9107fc120a1f7fe68d942f6848df1202 /jjb | |
parent | 86d0751bc220339dd27b585c771afd24b31c8876 (diff) | |
parent | dcc213dedc51a82832f90d644f14b28a3e55aa18 (diff) |
Merge "Add workaround for broken git repo polling by Jenkins"
Diffstat (limited to 'jjb')
-rw-r--r-- | jjb/ci-management/ci-management-coverity.yaml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/jjb/ci-management/ci-management-coverity.yaml b/jjb/ci-management/ci-management-coverity.yaml index fadea8882..6003bf24e 100644 --- a/jjb/ci-management/ci-management-coverity.yaml +++ b/jjb/ci-management/ci-management-coverity.yaml @@ -41,6 +41,7 @@ coverity-user-email: '' coverity-search-paths: '' coverity-search-exclude-regexs: '' + max-git-repo-age-hours: 0 stream: master submodule-recursive: true submodule-timeout: 10 @@ -101,6 +102,14 @@ name: DRY_RUN default: '{dry-run}' description: Do not submit results to Coverity Scan server at the end of the build. + - string: + name: 'MAX_GIT_REPO_AGE_HOURS' + default: '{max-git-repo-age-hours}' + description: > + If set to non-zero run the code scan only if there were no git + repository commits last MAX_GIT_REPO_AGE_HOURS hours. + It makes sense to set the value twice the 'cron' interval for the + job (e.g. if 'cron: @daily', then MAX_GIT_REPO_AGE_HOURS=48) triggers: - timed: '{obj:cron}' |