# HG changeset patch # User wenzelm # Date 1446835560 -3600 # Node ID d80eb8f6eb47a5166127f77ddf139f01f5f11b7c # Parent 976e546baddcdd1a7212f92026c6e978e051ff19 retain traditional rendering of \; diff -r 976e546baddc -r d80eb8f6eb47 etc/symbols --- a/etc/symbols Fri Nov 06 19:37:51 2015 +0100 +++ b/etc/symbols Fri Nov 06 19:46:00 2015 +0100 @@ -326,6 +326,7 @@ \ code: 0x0000aa \ code: 0x0000ba \
code: 0x0000a7 +\ code: 0x0000b6 \ code: 0x0000a1 \ code: 0x0000bf \ code: 0x0020ac @@ -359,7 +360,7 @@ \<^item> code: 0x0025aa group: control font: IsabelleText \<^enum> code: 0x0025b8 group: control font: IsabelleText \<^descr> code: 0x0027a7 group: control font: IsabelleText -\<^footnote> code: 0x0000b6 group: control +\<^footnote> code: 0x00204b group: control font: IsabelleText \<^verbatim> code: 0x0025a9 group: control font: IsabelleText \<^emph> code: 0x002217 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText