| commit | 8ffcb86771aad4a02a5b1672d286fc93bd355aea | [log] [tgz] |
|---|---|---|
| author | Davide Pesavento <davidepesa@gmail.com> | Sun Nov 20 20:22:11 2022 -0500 |
| committer | Davide Pesavento <davidepesa@gmail.com> | Sun Nov 20 20:22:11 2022 -0500 |
| tree | 883f127afd5f225708f6e596d5708bd9734f9325 | |
| parent | c6e4472df72d9ab71ed4ec6aff2ddaff231e7ce5 [diff] |
ci: skip headers check in code-coverage jobs Change-Id: I259a2a21c61da11805ccbd578a985c2ed764ef45
diff --git a/.jenkins b/.jenkins index 52b94c5..0f40e00 100755 --- a/.jenkins +++ b/.jenkins
@@ -26,7 +26,11 @@ esac export CACHE_DIR=${CACHE_DIR:-/tmp} -[[ $JOB_NAME == *"code-coverage" ]] && export DISABLE_ASAN=yes + +if [[ $JOB_NAME == *"code-coverage" ]]; then + export DISABLE_ASAN=yes + export DISABLE_HEADERS_CHECK=yes +fi for file in .jenkins.d/*; do [[ -f $file && -x $file ]] || continue