diff --git a/bin/test.sh b/bin/test.sh index 5290e0ac088e9b7d20f0dd14450aa26206e39f82..9acea71ddac95a62e2e42a00539115468e261f60 100755 --- a/bin/test.sh +++ b/bin/test.sh @@ -159,8 +159,8 @@ function TestAlias if [ "$DUNE_LOG" = "" ]; then Run dune build $DUNE_OPT $@ - elif [ "$SAVE" != "yes" ]; then - Run dune build $DUNE_OPT + elif [ "$SAVE" != "yes" ] && [ "$VERBOSE" != "yes" ]; then + Run dune build $DUNE_OPT $@ else # note: the Run function cannot performs redirection echo "> dune build $DUNE_OPT $@ 2> >(tee -a $DUNE_LOG >&2)"