Summary
- notes about old Java 8 font rendering for low-quality displays;
- obsolete -- was mostly about 'export_code';
- support both hinted and unhinted fonts;
The file was modified | src/Doc/JEdit/JEdit.thy (diff) |
The file was modified | src/Doc/JEdit/JEdit.thy (diff) |
The file was modified | Admin/components/components.sha1 (diff) |
The file was modified | Admin/components/main (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/Pure/Admin/build_fonts.scala (diff) |
The file was modified | src/Tools/jEdit/etc/options (diff) |