etc/symbols
changeset 56443 ee0f7cfb7bba
parent 56388 c771f0fe28d1
child 56591 1a59587f46ec
     1.1 --- a/etc/symbols	Sun Apr 06 17:19:08 2014 +0200
     1.2 +++ b/etc/symbols	Sun Apr 06 19:16:34 2014 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4  \<rat>                  code: 0x00211a  group: letter
     1.5  \<real>                 code: 0x00211d  group: letter
     1.6  \<int>                  code: 0x002124  group: letter
     1.7 -\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.  abbrev: <-
     1.8 +\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
     1.9  \<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
    1.10  \<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
    1.11  \<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->