| changeset 55786 | 96861130f922 |
| parent 55546 | 76979adf0b96 |
| child 56388 | c771f0fe28d1 |
--- a/etc/symbols Thu Feb 27 14:51:14 2014 +0100 +++ b/etc/symbols Thu Feb 27 17:24:16 2014 +0100 @@ -272,7 +272,7 @@ \<bar> code: 0x0000a6 group: punctuation abbrev: || \<plusminus> code: 0x0000b1 group: operator \<minusplus> code: 0x002213 group: operator -\<times> code: 0x0000d7 group: operator +\<times> code: 0x0000d7 group: operator abbrev: <*> \<div> code: 0x0000f7 group: operator \<cdot> code: 0x0022c5 group: operator \<star> code: 0x0022c6 group: operator