Skip to content
Snippets Groups Projects
Commit 26a27b8a authored by Thibault Martin's avatar Thibault Martin
Browse files

[tests] Concatenate DUNE_OPT the same way than dirs

parent f0fcbbd8
No related branches found
No related tags found
No related merge requests found
......@@ -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
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment