1.1 --- a/etc/symbols	Thu Feb 27 14:51:14 2014 +0100
     1.2 +++ b/etc/symbols	Thu Feb 27 17:24:16 2014 +0100
     1.3 @@ -272,7 +272,7 @@
     1.4  \<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
     1.5  \<plusminus>            code: 0x0000b1  group: operator
     1.6  \<minusplus>            code: 0x002213  group: operator
     1.7 -\<times>                code: 0x0000d7  group: operator
     1.8 +\<times>                code: 0x0000d7  group: operator  abbrev: <*>
     1.9  \<div>                  code: 0x0000f7  group: operator
    1.10  \<cdot>                 code: 0x0022c5  group: operator
    1.11  \<star>                 code: 0x0022c6  group: operator