author | wenzelm |
Fri, 30 Aug 2013 12:46:32 +0200 | |
changeset 53323 | 5fa77d6ad63d |
parent 53322 | a4cd032172e0 |
child 53324 | c12a3edcd8e4 |
etc/symbols | file | annotate | diff | comparison | revisions |
--- a/etc/symbols Fri Aug 30 12:44:39 2013 +0200 +++ b/etc/symbols Fri Aug 30 12:46:32 2013 +0200 @@ -277,7 +277,7 @@ \<cdot> code: 0x0022c5 group: operator \<star> code: 0x0022c6 group: operator \<bullet> code: 0x002219 group: operator -\<circ> code: 0x002218 group: operator abbrev: o +\<circ> code: 0x002218 group: operator \<dagger> code: 0x002020 \<ddagger> code: 0x002021 \<lhd> code: 0x0022b2 group: relation