New option -j <jobs>: no more than <jobs> simultaneously

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
             ;;