commit | 55bedb210fcadfab09b8205ba2263d9461cb782c | [log] [tgz] |
---|---|---|
author | Davide Pesavento <davidepesa@gmail.com> | Sat Dec 03 13:50:27 2022 -0500 |
committer | Davide Pesavento <davidepesa@gmail.com> | Sat Dec 03 13:50:27 2022 -0500 |
tree | 6360c2c1cbed3d868dcdb3552dbab06f9f8e2b87 | |
parent | c24147576e63bafb67d159d743cefca4a7304e83 [diff] [blame] |
build: update waf to version 2.0.24 Change-Id: Ibde735b40dc701f770433a04aaaa69917093de8b
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