mn200/HOL — Issue #40: Implement “smart quotes” for docfiles
Author: mn200
Created: 2011-10-12 10:48:36+00:00
State: open
Labels: Documentation, Feature Request

Currently we have to use back-quotes for `“` and double-apostrophes for `”` in order to make the LaTeX manuals work. Thus we get stuff like

This is a sentence with ``scare quotes''.

This results in ugly text in non-LaTeX places. Better would be to use normal quotes, and to then convert them as appropriate depending on the destination format. In fact, everywhere except LaTeX could use the Unicode characters. I don’t know if LaTeX supports Unicode quotation characters, though it might.