diff --git a/bin/test.sh b/bin/test.sh index 090a2fbfd5478ae26df3713ce7340c5fb0757e6f..35d0939f1777a0d5cddb2b925bd0144427f69411 100755 --- a/bin/test.sh +++ b/bin/test.sh @@ -194,7 +194,6 @@ do "--coverage") COVER=yes DUNE_OPT+="--workspace dev/dune-workspace.cover " - shift ;; "-n"|"--name") ALIAS_NAME=$2