commit | 054f3666812e97c625bb1746098d97064feb88c7 | [log] [tgz] |
---|---|---|
author | Davide Pesavento <davidepesa@gmail.com> | Tue Dec 06 15:10:23 2022 -0500 |
committer | Davide Pesavento <davidepesa@gmail.com> | Tue Dec 06 15:10:23 2022 -0500 |
tree | f96a26c0383a5190128189c208549740bc808cff | |
parent | f855ec1d12ab952aa7517b14600e2d52eba0d7f1 [diff] [blame] |
build: update waf to version 2.0.24 Change-Id: I18a730fd1fae017d4ee509ab44517b4646c18049
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