From cf97de74b90c7f9ed666fd02888ee76a694e19e8 Mon Sep 17 00:00:00 2001 From: flogth Date: Mon, 18 Sep 2023 21:45:23 +0200 Subject: [PATCH] fix direction of unicode arrows --- .../resources/unicode/unicode-latex-map | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/mmt-api/resources/unicode/unicode-latex-map b/src/mmt-api/resources/unicode/unicode-latex-map index 34011cb67..a0524699f 100644 --- a/src/mmt-api/resources/unicode/unicode-latex-map +++ b/src/mmt-api/resources/unicode/unicode-latex-map @@ -32,18 +32,18 @@ jlongleftrightarrow|⟷ jLongrightarrow|⟹ jLongleftarrow|⟸ jLongleftrightarrow|⟺ -jbla|↦ -jblA|⤇ -jblaa|⟼ -jblAA|⤇ -jbra|↤ -jbrA|⤆ -jbraa|⟻ -jbrAA|⤆ -jls|⇝ -jlss|⟿ -jrs|⇜ -jrss|⬳ +jbra|↦ +jbrA|⤇ +jbraa|⟼ +jbrAA|⤇ +jbla|↤ +jblA|⤆ +jblaa|⟻ +jblAA|⤆ +jrs|⇝ +jrss|⟿ +jls|⇜ +jlss|⬳ jmapsto|↦ jMapsto|⤇ jlongmapsto|⟼