diff --git a/bin/test.sh b/bin/test.sh index a79dd8ffc588c1093aae80ae3d5128b934f3e223..e32546cf0bdcbc954f2c5d611c94a97ab6516835 100755 --- a/bin/test.sh +++ b/bin/test.sh @@ -315,6 +315,8 @@ function PrepareCoverage Cmd rm -rf _bisect Cmd mkdir _coverage Cmd mkdir _bisect + + DUNE_OPT+="--workspace dev/dune-workspace.cover " fi } @@ -371,9 +373,6 @@ function PrepareTests [ "$DUNE_LOG" = "" ] || rm -rf $DUNE_LOG function RunAlias { - if [ "$COVER" = "yes" ]; then - DUNE_OPT+="--workspace dev/dune-workspace.cover " - fi Head "Running tests..." if [ "$DUNE_LOG" = "" ]; then Run dune build $DUNE_OPT $@