diff options
| author | Gaëtan Gilbert | 2019-02-14 14:57:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 21:24:11 +0100 |
| commit | 2e4e082637771bc047fbd977aaa5de26956c4618 (patch) | |
| tree | 10c4dcfda4047eeff0d9859c32df9c51142b8eb4 /doc | |
| parent | 7c4d6b904adb4a5d025ebcb804613f558e5b8be9 (diff) | |
coqdomain.py fix typo in comment
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 791953eeaf..2d8bb43e62 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -882,7 +882,7 @@ class CoqtopBlocksTransform(Transform): dli = nodes.definition_list_item() for sentence, output in pairs: - # Use Coqdoq to highlight input + # Use Coqdoc to highlight input in_chunks = highlight_using_coqdoc(sentence) dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input)) # Parse ANSI sequences to highlight output |