diff options
| -rwxr-xr-x | scripts/checkhelp.awk | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/scripts/checkhelp.awk b/scripts/checkhelp.awk index 1a7e0ea8e..85d0661a7 100755 --- a/scripts/checkhelp.awk +++ b/scripts/checkhelp.awk @@ -23,6 +23,9 @@ /^[[:space:]]*help[[:space:]]*$/ { help[pos] = 1; } +/^[[:space:]]*bool[[:space:]]*$/ { + help[pos] = 1; # ignore options which are not selectable +} BEGIN { pos = -1; is_choice = 0; |