aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJim Fehrle2020-04-17 12:26:28 -0700
committerJim Fehrle2020-04-19 09:27:28 -0700
commit796878d827693fefdfe4901af7a71bfe20f2011c (patch)
tree83469fd75716a662bdebd6455071856d705013b3
parentf3af9a4c6e6813f32dfe632209e145ffbf5fed98 (diff)
Don't create index entries for the name "_"
-rw-r--r--doc/tools/coqrst/coqdomain.py15
1 files changed, 7 insertions, 8 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index b448d0f9d3..57243207f0 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -188,20 +188,19 @@ class CoqObject(ObjectDescription):
def _add_index_entry(self, name, target):
"""Add `name` (pointing to `target`) to the main index."""
assert isinstance(name, str)
- if not name.startswith("_"):
- # remove trailing . , found in commands, but not ... (ellipsis)
- trim = name.endswith(".") and not name.endswith("...")
- index_text = name[:-1] if trim else name
- if self.index_suffix:
- index_text += " " + self.index_suffix
- self.indexnode['entries'].append(('single', index_text, target, '', None))
+ # remove trailing . , found in commands, but not ... (ellipsis)
+ trim = name.endswith(".") and not name.endswith("...")
+ index_text = name[:-1] if trim else name
+ if self.index_suffix:
+ index_text += " " + self.index_suffix
+ self.indexnode['entries'].append(('single', index_text, target, '', None))
aliases = None # additional indexed names for a command or other object
def add_target_and_index(self, name, _, signode):
"""Attach a link target to `signode` and an index entry for `name`.
This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified."""
- if name:
+ if name and not (isinstance(name, str) and name.startswith('_')):
target = self._add_target(signode, name)
self._add_index_entry(name, target)
if self.aliases is not None: