changeset 63733 | 7dc86a284456 |
parent 63677 | be8b557ec73e |
child 64556 | 851ae0e7b09c |
--- a/etc/symbols Tue Aug 30 09:04:40 2016 +0200 +++ b/etc/symbols Tue Aug 30 14:47:23 2016 +0200 @@ -385,3 +385,4 @@ \<^dir> code: 0x01F5C0 group: icon font: IsabelleText \<^url> code: 0x01F310 group: icon font: IsabelleText \<^doc> code: 0x01F4D3 group: icon font: IsabelleText +\<^action> code: 0x00261b group: icon font: IsabelleText