etc/symbols
changeset 53073 1835a83309d6
parent 53021 d0fa3f446b9d
child 53194 1943db7bc34c
     1.1 --- a/etc/symbols	Sun Aug 18 15:31:12 2013 +0200
     1.2 +++ b/etc/symbols	Sun Aug 18 15:33:26 2013 +0200
     1.3 @@ -350,9 +350,9 @@
     1.4  \<cedilla>              code: 0x0000b8
     1.5  \<hungarumlaut>         code: 0x0002dd
     1.6  \<some>                 code: 0x0003f5
     1.7 -\<^sub>                 code: 0x0021e9  group: control  font: IsabelleText  abbrev: =_
     1.8 -\<^sup>                 code: 0x0021e7  group: control  font: IsabelleText  abbrev: =^
     1.9 -\<^bold>                code: 0x002759  group: control  font: IsabelleText  abbrev: -.
    1.10 +\<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
    1.11 +\<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
    1.12 +\<^bold>                code: 0x002759  group: control  font: IsabelleText
    1.13  \<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
    1.14  \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
    1.15  \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(