diff options
| author | Jim Fehrle | 2020-02-16 13:17:20 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-02-16 13:17:20 -0800 |
| commit | 8b58b887a95f0abfac16e8dc6f5e68f21e99ef31 (patch) | |
| tree | b7fb12450f72c757db18d363c35e330f13ae4954 /doc | |
| parent | 2e36df827c85ea93cc7614dc25f82a16f72e6e9d (diff) | |
Show apostrophes and backticks in HTML, too.
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("'") |