receovered alternative abbrevs for \<open> \<close> from 8e8243975860, to accommodate national keyboard layouts where "`" might be hard to produce;
authorwenzelm
Sat, 24 May 2014 12:58:22 +0200
changeset 57081 5fc1c2098964
parent 57080 0e5fa27d3293
child 57082 2c1c8b38e3f0
receovered alternative abbrevs for \<open> \<close> from 8e8243975860, to accommodate national keyboard layouts where "`" might be hard to produce;
etc/symbols
--- a/etc/symbols	Sat May 24 12:55:09 2014 +0200
+++ b/etc/symbols	Sat May 24 12:58:22 2014 +0200
@@ -348,8 +348,8 @@
 \<hungarumlaut>         code: 0x0002dd
 \<some>                 code: 0x0003f5
 \<newline>              code: 0x0023ce
-\<open>                 code: 0x002039  group: punctuation  font: IsabelleText
-\<close>                code: 0x00203a  group: punctuation  font: IsabelleText
+\<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
+\<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
 \<here>                 code: 0x002302  font: IsabelleText
 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
 \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText