# HG changeset patch # User wenzelm # Date 1454588507 -3600 # Node ID f82f6c7476a1f4faafd2c84e57ba2fcb19136227 # Parent 7afbd7fc32fd55782cc2b0ed4a1120675e8792f8 clarified; diff -r 7afbd7fc32fd -r f82f6c7476a1 etc/symbols --- a/etc/symbols Thu Feb 04 12:11:27 2016 +0100 +++ b/etc/symbols Thu Feb 04 13:21:47 2016 +0100 @@ -357,7 +357,7 @@ \ code: 0x0003f5 \ code: 0x002311 \ code: 0x0023ce -\ code: 0x002015 font: IsabelleText +\ code: 0x002015 group: document font: IsabelleText \ code: 0x002039 group: punctuation font: IsabelleText abbrev: << \ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \ code: 0x002302 font: IsabelleText