diff options
| author | Théo Zimmermann | 2020-02-17 14:49:54 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-17 14:49:54 +0100 |
| commit | e7384ffaf290cb01eba1df12d3e13ddd9a4b3c92 (patch) | |
| tree | 5cedbb5ff546a9cd469bc2acd1449ba113e99c6e /doc | |
| parent | cd7323ce0f7648f6db732292c0ded05c480be71f (diff) | |
| parent | 8b58b887a95f0abfac16e8dc6f5e68f21e99ef31 (diff) | |
Merge PR #11614: Show apostrophes and backticks in HTML doc, too.
Reviewed-by: Zimmi48
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/tools/coqrst/notations/sphinx.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index ab18d136b8..5659a64b84 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -80,9 +80,11 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): while atom != "": if atom[0] == "'": node += nodes.raw("\\textquotesingle{}", "\\textquotesingle{}", format="latex") + node += nodes.raw("'", "'", format="html") atom = atom[1:] elif atom[0] == "`": node += nodes.raw("\\`{}", "\\`{}", format="latex") + node += nodes.raw("`", "`", format="html") atom = atom[1:] else: index_ap = atom.find("'") |