LaTeX munger on character literals

[xrchz]

Default printing of character literals uses a hash (#), which does not work well inside LaTeX documents. Character literals should be treated like other literals (i.e. specially), probably using a \HOLCharLit{} command.