diff options
| author | Théo Zimmermann | 2020-02-14 17:58:42 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-14 17:58:42 +0100 |
| commit | bdc8e29d806ab7e9bbd0491bf237890b7934795a (patch) | |
| tree | 648c00bb0871e86d9f2ecf9dcc76f4d28a528eba /dev | |
| parent | df94f1a5430dde7cee6ccb1c16854bcbc94575c8 (diff) | |
| parent | b1f54040c04743082e63a3222ea003b00653b176 (diff) | |
Merge PR #11599: Spell out index entry suffixes in main index, e.g. "(tactic)" instead of "(tacn)"
Reviewed-by: Zimmi48
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions