diff options
| -rwxr-xr-x | tools/make-directive-index.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/make-directive-index.py b/tools/make-directive-index.py index 5b965f4163..da10575f32 100755 --- a/tools/make-directive-index.py +++ b/tools/make-directive-index.py @@ -187,6 +187,9 @@ def _extract_directives(directive_groups, formatting, page): storvar if klass else storopt)): for name in variablelist.iterfind(xpath): text = re.sub(r'([= ]).*', r'\1', name.text).rstrip() + if text.startswith('-'): + # for options, merge options with and without mandatory arg + text = text.partition('=')[0] stor[text].append((pagename, section)) if text not in formatting: # use element as formatted display |