commit | 5379589ea623d9d6bf083bd82d3d423d0a22cc8b | [log] [tgz] |
---|---|---|
author | Davide Pesavento <davidepesa@gmail.com> | Mon Dec 12 15:14:04 2022 -0500 |
committer | Davide Pesavento <davidepesa@gmail.com> | Mon Dec 12 15:14:04 2022 -0500 |
tree | 0051b84989e6929ca2ff0e10d12930328924725c | |
parent | b2034db9180f916d966797989112925f75d0e330 [diff] [blame] |
build: update waf to version 2.0.24 Change-Id: I1f13168122da17d33a8da9547ad6ff6555d9f4ae
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