| commit | b5e95f9106d4f8c193a7bd53984871f01bca7be0 | [log] [tgz] |
|---|---|---|
| author | Davide Pesavento <davidepesa@gmail.com> | Sun Nov 20 20:16:06 2022 -0500 |
| committer | Davide Pesavento <davidepesa@gmail.com> | Sun Nov 20 20:16:06 2022 -0500 |
| tree | 4ed407edafb3a6626b8821b7741a65054a440552 | |
| parent | 83faec7308d8a98b45f967ba2693ed4c9c2de034 [diff] |
ci: skip headers check in code-coverage jobs Change-Id: I73f5cc04cc4b8bf69db66e690d9d4117239a0961
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