diff options
author | Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> | 2013-02-27 21:31:02 -0500 |
---|---|---|
committer | Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> | 2013-02-27 21:55:00 -0500 |
commit | 699ad6c06c0e235f588c900934bdf4bed421503b (patch) | |
tree | 8b37106960b3f91a6275f966692b6cb6958286a5 /make-directive-index.py | |
parent | 185c3be03cec26023acc11b49553753aa7330a1d (diff) |
man: drop rhs parts in snippets in directive index
- --exit-if-exists=file
+ --exit-if-exists=
etc.
Diffstat (limited to 'make-directive-index.py')
-rwxr-xr-x | make-directive-index.py | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/make-directive-index.py b/make-directive-index.py index 15bd9b9341..c61383b0a4 100755 --- a/make-directive-index.py +++ b/make-directive-index.py @@ -185,7 +185,10 @@ def _extract_directives(directive_groups, formatting, page): stor[text].append((pagename, section)) if text not in formatting: # use element as formatted display - name.tail = '' + if name.text[-1] in '= ': + name.clear() + else: + name.tail = '' name.text = text formatting[text] = name |