commit d4689c8f805c2c0ba38fab3e44519c55316c1ac9
author Davide Pesavento <davidepesa@gmail.com> Thu Oct 07 02:53:03 2021 -0400
committer Davide Pesavento <davidepesa@gmail.com> Thu Oct 07 02:53:03 2021 -0400
tree f585ce5243fa039724e5966c820ad1605987e680
parent 80b50fbd1e3dd7d6e66ce43fb6ef477edc04499d

build: make examples optional

Change-Id: Ia57725bbe0e921c145f153c5395ed60436c8782a

.jenkins.d/10-build.sh

diff --git a/.jenkins.d/10-build.sh b/.jenkins.d/10-build.sh
index 20e6bd1..692ad2f 100755
--- a/.jenkins.d/10-build.sh
+++ b/.jenkins.d/10-build.sh
@@ -27,8 +27,8 @@
     ./waf --color=yes distclean
 fi
 
-# Build in debug mode with tests
-./waf --color=yes configure --debug --with-tests $ASAN $COVERAGE
+# Build in debug mode with tests and examples
+./waf --color=yes configure --debug --with-tests --with-examples $ASAN $COVERAGE
 ./waf --color=yes build -j$WAF_JOBS
 
 # (tests will be run against the debug version)