clarified abbrev;
authorwenzelm
Fri, 01 Jan 2016 11:27:29 +0100
changeset 62025 8007e4ff493a
parent 62024 e3e22a5e85f2
child 62026 ea3b1b0413b4
clarified abbrev;
etc/symbols
--- a/etc/symbols	Fri Jan 01 11:18:54 2016 +0100
+++ b/etc/symbols	Fri Jan 01 11:27:29 2016 +0100
@@ -352,7 +352,7 @@
 \<dieresis>             code: 0x0000a8
 \<cedilla>              code: 0x0000b8
 \<hungarumlaut>         code: 0x0002dd
-\<bind>                 code: 0x00291c  abbrev: >>  abbrev: >>=
+\<bind>                 code: 0x00291c  abbrev: >>=
 \<then>                 code: 0x002aa2  abbrev: >>
 \<some>                 code: 0x0003f5
 \<hole>                 code: 0x002311