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