# HG changeset patch
# User wenzelm
# Date 1444908528 -7200
# Node ID 7cf8b604280f21cd374dbd76c05c72ca6ac98e22
# Parent  9b09acfb7e06cb078ed91b922c2ab78f694bb23c
unused -- avoid confusion in Symbols dockable;

diff -r 9b09acfb7e06 -r 7cf8b604280f etc/symbols
--- a/etc/symbols	Thu Oct 15 13:28:36 2015 +0200
+++ b/etc/symbols	Thu Oct 15 13:28:48 2015 +0200
@@ -359,7 +359,7 @@
 \<^item>                code: 0x0025aa  group: control  font: IsabelleText
 \<^enum>                code: 0x0025b8  group: control  font: IsabelleText
 \<^descr>               code: 0x0027a7  group: control  font: IsabelleText
-\<^emph>                code: 0x002217  group: control  font: IsabelleText
+#\<^emph>                code: 0x002217  group: control  font: IsabelleText
 \<^bold>                code: 0x002759  group: control  font: IsabelleText
 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
 \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText