From 2468f25c33a9ce8a4d24d217820bb731b1232600 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Tue, 7 Dec 2010 11:05:10 -0600 Subject: [PATCH] Adds support for inserting more arrow characters by their LaTex names original commit: a12491bb89030eda9635e0a1925dd60c8ea6d668 --- collects/mrlib/tex-table.rkt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/collects/mrlib/tex-table.rkt b/collects/mrlib/tex-table.rkt index 25c0f9d6..5d5c65a3 100644 --- a/collects/mrlib/tex-table.rkt +++ b/collects/mrlib/tex-table.rkt @@ -28,15 +28,15 @@ ("leftrightarrow" "↔") ("nearrow" "↗") ("Updownarrow" "⇕") - + ("hookleftarrow" "↩") + ("hookrightarrow" "↪") + ("leadsto""↝") + ;; arrows that didn't come out right in copy & paste ;←− \longleftarrow ;⇐= \Longleftarrow - ;← 􏰂 \hookleftarrow ;←→ \longleftrightarrow - ;􏰁 → \hookrightarrow ;⇐⇒ \Longleftrightarrow - ;􏴲 \leadsto∗ ;􏰃−→ \longmapsto ;=⇒ \Longrightarrow ;􏰃→ \mapsto