diff --git a/Jenkinsfile b/Jenkinsfile index 541c411794825d4ec858ac1b67b0ead928f435dd..31f0b22be06ee659cdb5e1959bff625dd2675aa9 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -178,7 +178,8 @@ def make_build(label, board, desc, arg) for app in ${apps}; do if [[ \$(make -sC \$app info-boards-supported | tr ' ' '\n' | sed -n '/^${board}\$/p') ]]; then echo \"\n\nBuilding \$app for ${board}\" >> success_${board}_${desc}.log - make -j\${NPROC} -C \$app all >> success_${board}_${desc}.log 2>&1 || RESULT=1 + rm -rf jenkins_bin; mkdir jenkins_bin + CFLAGS_DBG=\"\" BINDIR=\$(pwd)/jenkins_bin make -j\${NPROC} -C \$app all >> success_${board}_${desc}.log 2>&1 || RESULT=1 fi; done; if ((\$RESULT)); then