From bef67ce780546918f5b7f8c46c6fe34b2248b7f0 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 24 Jul 2023 11:21:36 +0200
Subject: [PATCH] New option -j <jobs>: no more than <jobs> simultaneously
---
bin/test.sh | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/bin/test.sh b/bin/test.sh
index f38975ea98c..72742e38f57 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
;;
--
GitLab