Sat, 24 Nov 2012 18:29:19 +0100 | wenzelm | tuned -- Symbol.groups already sorted; | changeset | files |
Sat, 24 Nov 2012 17:46:54 +0100 | wenzelm | more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs; | changeset | files |