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|⟼