From 26a27b8ab67944f02dcd0bb10972d9e086cda3f5 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 18 Apr 2024 15:26:19 +0200
Subject: [PATCH] [tests] Concatenate DUNE_OPT the same way than dirs
---
bin/test.sh | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/bin/test.sh b/bin/test.sh
index 06c523c4e9f..913dc6b960d 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -179,22 +179,22 @@ do
PULLCACHE=yes
;;
"-f"|"--force")
- DUNE_OPT+="--force "
+ DUNE_OPT+=" --force"
;;
"-u"|"--update")
- DUNE_OPT+="--auto-promote "
+ DUNE_OPT+=" --auto-promote"
UPDATE=yes
;;
"--watch")
- DUNE_OPT+="--watch "
+ DUNE_OPT+=" --watch"
;;
"-v"|"--verbose")
- DUNE_OPT+="--display=short "
+ DUNE_OPT+=" --display=short"
VERBOSE=yes
;;
"-j"|"--jobs")
if [[ $2 == "auto" ]] || ([[ $2 != \-* ]] && [[ $2 -ge 1 ]]); then
- DUNE_OPT+="-j $2 "
+ DUNE_OPT+=" -j $2"
shift
else
ErrorUsage \
@@ -316,7 +316,7 @@ function PrepareCoverage
Cmd mkdir _coverage
Cmd mkdir _bisect
- DUNE_OPT+="--workspace dev/dune-workspace.cover "
+ DUNE_OPT+=" --workspace dev/dune-workspace.cover"
fi
}
--
GitLab