diff --git a/bin/test.sh b/bin/test.sh index f38975ea98ce8a7386b49ee80f44f18e8f345595..72742e38f578cd3e52b626c52829edc09b1b380e 100755 --- a/bin/test.sh +++ b/bin/test.sh @@ -74,6 +74,7 @@ function Usage echo " -u|--update run tests and update oracles (and WP-cache)" echo " -s|--save save dune logs into $DUNE_LOG" echo " -v|--verbose print executed commands" + echo " -j|--jobs <jobs> Run no more than <jobs> commands simultaneously." echo " -h|--help print this help" echo "" echo "VARIABLES" @@ -155,13 +156,22 @@ do PULLCACHE=yes ;; "-u"|"--update") - DUNE_OPT+="--auto-promote" + DUNE_OPT+="--auto-promote " UPDATE=yes ;; "-v"|"--verbose") - DUNE_OPT+="--display=short" + DUNE_OPT+="--display=short " VERBOSE=yes ;; + "-j"|"--jobs") + if [[ $2 != \-* ]] && [ "$2" -ge 1 ]; then + DUNE_OPT+="-j $2 " + shift + else + ErrorUsage \ + "wrong argument ('$2') for '-j|--jobs', int >= 1 expected" + fi + ;; "-l"|"--logs") LOGS=yes ;;