# HG changeset patch
# User wenzelm
# Date 1446716137 -3600
# Node ID f06e5a5a4b46ba88cd83dbdba6ce8cf12ea85f02
# Parent  c2b7033fa0ba2c10b915f6ff650bbb43935b8b28
IsabelleText for unusual symbol;

diff -r c2b7033fa0ba -r f06e5a5a4b46 etc/symbols
--- a/etc/symbols	Thu Nov 05 10:34:34 2015 +0100
+++ b/etc/symbols	Thu Nov 05 10:35:37 2015 +0100
@@ -348,7 +348,7 @@
 \<some>                 code: 0x0003f5
 \<hole>                 code: 0x002311
 \<newline>              code: 0x0023ce
-\<comment>              code: 0x002015
+\<comment>              code: 0x002015  font: IsabelleText
 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
 \<here>                 code: 0x002302  font: IsabelleText