diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/scripts/init.sh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh index 9969a82ec..0ef5c219e 100755 --- a/tools/ci/scripts/init.sh +++ b/tools/ci/scripts/init.sh @@ -188,7 +188,8 @@ function run_make { export JOBS=2 echo "No JOBS defined" fi - + echo make clean + make clean || true echo "make -j${JOBS} V=0 $*" make -j${JOBS} V=0 $* 2>$ERRFILE check_error $? @@ -200,6 +201,8 @@ function run_make_check { export JOBS=2 echo "No JOBS defined" fi + echo make clean + make clean || true echo "make -j${JOBS} V=0 check $*" make -j${JOBS} V=0 check $* 2>$ERRFILE export ERR=$? |