diff options
| author | Jim Fehrle | 2020-04-17 12:26:28 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-04-19 09:27:28 -0700 |
| commit | 796878d827693fefdfe4901af7a71bfe20f2011c (patch) | |
| tree | 83469fd75716a662bdebd6455071856d705013b3 | |
| parent | f3af9a4c6e6813f32dfe632209e145ffbf5fed98 (diff) | |
Don't create index entries for the name "_"
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 15 |
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: |
