diff options
| -rwxr-xr-x | scripts/dox_to_sphinx.py | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/scripts/dox_to_sphinx.py b/scripts/dox_to_sphinx.py index c9d401cc..3842586d 100755 --- a/scripts/dox_to_sphinx.py +++ b/scripts/dox_to_sphinx.py @@ -257,6 +257,12 @@ def dox_to_rst(index, lang, node): return " " + markup.strip() + if node.tag == "lsquo": + return "‘" + + if node.tag == "rsquo": + return "’" + if node.tag == "computeroutput": # assert len(node) == 0 FIXME return "``%s``" % node.text |