scribble: another Unicode mapping for Latex output
This mapping is needed by the "redex-unstable" documentation. Merge to v6.1
This commit is contained in:
parent
09b4445c7a
commit
a33c64b45f
|
@ -1002,6 +1002,8 @@
|
||||||
[(#\”) "{''}"]
|
[(#\”) "{''}"]
|
||||||
[(#\u2013) "{--}"]
|
[(#\u2013) "{--}"]
|
||||||
[(#\u2014) "{---}"]
|
[(#\u2014) "{---}"]
|
||||||
|
[(#\〈) "$\\langle$"]
|
||||||
|
[(#\〉) "$\\rangle$"]
|
||||||
[(#\∞) "$\\infty$"]
|
[(#\∞) "$\\infty$"]
|
||||||
[(#\⇓) "$\\Downarrow$"]
|
[(#\⇓) "$\\Downarrow$"]
|
||||||
[(#\↖) "$\\nwarrow$"]
|
[(#\↖) "$\\nwarrow$"]
|
||||||
|
|
Loading…
Reference in New Issue
Block a user