From 0323df083efe54d1558809a17d4565069a65bc01 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 10 Sep 2024 15:22:39 +0200
Subject: [PATCH] [script] Add option --, all following args are passed to dune
---
bin/test.sh | 22 ++++++++++++++++++----
1 file changed, 18 insertions(+), 4 deletions(-)
diff --git a/bin/test.sh b/bin/test.sh
index 41b9e0e96ba..d0e022d771d 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -38,6 +38,7 @@ JSON=
DUNE_ALIAS=
DUNE_OPT=
+DUNE_OPT_POST=
DUNE_LOG=./.test-errors.log
ALIAS_NAME=ptests
LOCAL_WP_CACHE=$(pwd -P)/.wp-cache
@@ -88,6 +89,12 @@ function Usage
echo " --coverage-json compute test coverage in Coveralls JSON format"
echo " -h|--help print this help"
echo ""
+ echo "TRAILING OPTIONS"
+ echo ""
+ echo " All arguments passed after a double dash '--' are passed to dune"
+ echo " For example in 'test.sh -r -u tests -- -j 12', '-j 12' will be"
+ echo " passed as a dune argument"
+ echo ""
echo "VARIABLES"
echo ""
echo " FRAMAC_WP_CACHE"
@@ -224,6 +231,10 @@ do
"eva")
TESTS+=" tests/value tests/builtins tests/float tests/idct"
;;
+ "--")
+ shift
+ break
+ ;;
*)
if [ -f $1 ] || [ -d $1 ]; then
TESTS+=" $1"
@@ -239,6 +250,9 @@ do
shift
done
+# Pass all the remaining options (after '--') to dune at the end of the command
+DUNE_OPT_POST="$@"
+
# --------------------------------------------------------------------------
# --- WP Cache Environment
# --------------------------------------------------------------------------
@@ -398,13 +412,13 @@ function RunAlias
{
Head "Running tests..."
if [ "$DUNE_LOG" = "" ]; then
- Run dune build $DUNE_OPT $@
+ Run dune build $DUNE_OPT $@ $DUNE_OPT_POST
elif [ "$SAVE" != "yes" ] && [ "$VERBOSE" != "yes" ]; then
- Run dune build $DUNE_OPT $@
+ Run dune build $DUNE_OPT $@ $DUNE_OPT_POST
else
# note: the Run function cannot performs redirection
- echo "> dune build $DUNE_OPT $@ 2> >(tee -a $DUNE_LOG >&2)"
- dune build $DUNE_OPT $@ 2> >(tee -a $DUNE_LOG >&2)
+ echo "> dune build $DUNE_OPT $@ $DUNE_OPT_POST 2> >(tee -a $DUNE_LOG >&2)"
+ dune build $DUNE_OPT $@ $DUNE_OPT_POST 2> >(tee -a $DUNE_LOG >&2)
fi
}
--
GitLab