scribble: another Unicode mapping for Latex output

This mapping is needed by the "redex-unstable" documentation.

Merge to v6.1

original commit: a33c64b45f54404c50741f04137c62fbe5c4efe2
This commit is contained in:
Matthew Flatt 2014-07-18 07:39:33 +01:00
parent ee3af7611f
commit 52917bc3ec

View File

@ -1002,6 +1002,8 @@
[(#\”) "{''}"]
[(#\u2013) "{--}"]
[(#\u2014) "{---}"]
[(#\〈) "$\\langle$"]
[(#\〉) "$\\rangle$"]
[(#\∞) "$\\infty$"]
[(#\⇓) "$\\Downarrow$"]
[(#\↖) "$\\nwarrow$"]