From a58755b6173355b61d3d5b77e3ae2cb6dbc8c25a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 3 Aug 2023 15:40:20 +0200
Subject: [PATCH] [tests] Fixes script test.sh: option --coverage does not
expect an argument.
---
bin/test.sh | 1 -
1 file changed, 1 deletion(-)
diff --git a/bin/test.sh b/bin/test.sh
index 090a2fbfd54..35d0939f177 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
--
GitLab