diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/scripts/init.sh | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh index 77e03ec76..a2aac226e 100755 --- a/tools/ci/scripts/init.sh +++ b/tools/ci/scripts/init.sh @@ -184,15 +184,22 @@ function run_cmake { function run_make { rm $ERRFILE - echo "make -j2 V=0 $*" - make -j2 V=0 $* 2>$ERRFILE + if [ "$JOBS" == "" ]; + export JOBS=2 + fi + + echo "make -j${JOBS} V=0 $*" + make -j${JOBS} V=0 $* 2>$ERRFILE check_error $? } function run_make_check { rm $ERRFILE - echo "make -j2 V=0 check $*" - make -j2 V=0 check $* 2>$ERRFILE + if [ "$JOBS" == "" ]; + export JOBS=2 + fi + echo "make -j${JOBS} V=0 check $*" + make -j${JOBS} V=0 check $* 2>$ERRFILE export ERR=$? if [ "${ERR}" != 0 ]; then cat $ERRFILE |