changeset 62022 | 7a6ae107ec3c |
parent 61972 | a70b89a3e02e |
child 62023 | 19605292757e |
--- a/etc/symbols Fri Jan 01 11:07:07 2016 +0100 +++ b/etc/symbols Fri Jan 01 11:07:29 2016 +0100 @@ -352,6 +352,8 @@ \<dieresis> code: 0x0000a8 \<cedilla> code: 0x0000b8 \<hungarumlaut> code: 0x0002dd +\<bind> code: 0x00291c abbrev: >> abbrev: >>= +\<then> code: 0x002aa2 abbrev: >> \<some> code: 0x0003f5 \<hole> code: 0x002311 \<newline> code: 0x0023ce