# 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 @@ \ code: 0x0003f5 \ code: 0x002311 \ code: 0x0023ce -\ code: 0x002015 +\ code: 0x002015 font: IsabelleText \ code: 0x002039 group: punctuation font: IsabelleText abbrev: << \ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \ code: 0x002302 font: IsabelleText