| commit | 59f6fabe5086fc8bbcc38b82933c6bc79c869cef | [log] [tgz] |
|---|---|---|
| author | Davide Pesavento <davidepesa@gmail.com> | Fri Dec 02 20:36:32 2022 -0500 |
| committer | Davide Pesavento <davidepesa@gmail.com> | Fri Dec 02 20:36:32 2022 -0500 |
| tree | c7043ddde28f87c787426891cde79d45e67fca50 | |
| parent | 737f2de0bdaf220f133083d4e902f26f0d898ba7 [diff] [blame] |
build: update waf to version 2.0.24 Change-Id: I3b7226af85fa686d33866899a9c2e487313fc842
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