etc/symbols
changeset 59974 b911c8ba0b69
parent 57081 5fc1c2098964
child 61405 d2ce32c5793a
     1.1 --- a/etc/symbols	Wed Apr 08 20:41:56 2015 +0200
     1.2 +++ b/etc/symbols	Wed Apr 08 21:08:26 2015 +0200
     1.3 @@ -347,6 +347,7 @@
     1.4  \<cedilla>              code: 0x0000b8
     1.5  \<hungarumlaut>         code: 0x0002dd
     1.6  \<some>                 code: 0x0003f5
     1.7 +\<hole>                 code: 0x002311
     1.8  \<newline>              code: 0x0023ce
     1.9  \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
    1.10  \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
    1.11 @@ -358,4 +359,3 @@
    1.12  \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
    1.13  \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
    1.14  \<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
    1.15 -