# HG changeset patch
# User wenzelm
# Date 1390160388 -3600
# Node ID 5f4d5f6876f120cbebe62e646f51435caa14eb71
# Parent  acefda71629bec3b6dfe87649302f6d481aaa2ab
group symbols;

diff -r acefda71629b -r 5f4d5f6876f1 etc/symbols
--- a/etc/symbols	Sun Jan 19 11:05:38 2014 +0100
+++ b/etc/symbols	Sun Jan 19 20:39:48 2014 +0100
@@ -348,8 +348,8 @@
 \<hungarumlaut>         code: 0x0002dd
 \<some>                 code: 0x0003f5
 \<newline>              code: 0x0023ce
-\<open>                 code: 0x002039  abbrev: <<  font: IsabelleText
-\<close>                code: 0x00203a  abbrev: >>  font: IsabelleText
+\<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
+\<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
 \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
 \<^bold>                code: 0x002759  group: control  font: IsabelleText