etc/symbols
changeset 61579 634cd44bb1d3
parent 61571 9c50eb3bff50
child 61584 f06e5a5a4b46
--- a/etc/symbols	Wed Nov 04 23:27:00 2015 +0100
+++ b/etc/symbols	Thu Nov 05 00:02:30 2015 +0100
@@ -348,6 +348,7 @@
 \<some>                 code: 0x0003f5
 \<hole>                 code: 0x002311
 \<newline>              code: 0x0023ce
+\<comment>              code: 0x002015
 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
 \<here>                 code: 0x002302  font: IsabelleText