diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/scripts/init.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh index 3bad16408..99e6e2ac5 100755 --- a/tools/ci/scripts/init.sh +++ b/tools/ci/scripts/init.sh @@ -186,6 +186,7 @@ function run_make { rm $ERRFILE if [ "$JOBS" == "" ]; then export JOBS=2 + echo "No JOBS defined" fi echo "make -j${JOBS} V=0 $*" @@ -197,6 +198,7 @@ function run_make_check { rm $ERRFILE if [ "$JOBS" == "" ]; then export JOBS=2 + echo "No JOBS defined" fi echo "make -j${JOBS} V=0 check $*" make -j${JOBS} V=0 check $* 2>$ERRFILE |