From 235fd786020eedca8fcbb3756b8f3cc72a8e2358 Mon Sep 17 00:00:00 2001 From: Steven Murdoch Date: Thu, 26 May 2022 15:12:36 +0000 Subject: [PATCH] Fix "coverage -h" command $SCRIPT_NAME is not defined so causes an error. Use $(basename "$0") instead. --- maint/coverage | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/maint/coverage b/maint/coverage index 8f088011e..b0f66b2f3 100755 --- a/maint/coverage +++ b/maint/coverage @@ -3,7 +3,7 @@ function usage() { cat <