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;