From 81b59f48d29f8edc1ad1d16a4498f1e825e9bd91 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 26 Jul 2023 17:36:42 +0200
Subject: [PATCH] [tests] document coverage option
---
bin/test.sh | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/bin/test.sh b/bin/test.sh
index 39cc55d2ff0..5b2da558ae5 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -75,7 +75,8 @@ function Usage
echo " -u|--update run tests and update oracles (and WP-cache)"
echo " -s|--save save dune logs into $DUNE_LOG"
echo " -v|--verbose print executed commands"
- echo " -j|--jobs <jobs> Run no more than <jobs> commands simultaneously."
+ echo " -j|--jobs <jobs> run no more than <jobs> commands simultaneously."
+ echo " --coverage compute test coverage"
echo " -h|--help print this help"
echo ""
echo "VARIABLES"
--
GitLab