Skip to content
Failed

Changes

Summary

  1. notes about old Java 8 font rendering for low-quality displays;
  2. obsolete -- was mostly about 'export_code';
  3. support both hinted and unhinted fonts;
Changeset 70074:b718a64d0d09 by wenzelm:
notes about old Java 8 font rendering for low-quality displays;
The file was modified src/Doc/JEdit/JEdit.thy (diff)
Changeset 70073:6b0e4ba2062c by wenzelm:
obsolete -- was mostly about 'export_code';
The file was modified src/Doc/JEdit/JEdit.thy (diff)
Changeset 70072:54dc58086351 by wenzelm:
support both hinted and unhinted fonts;
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)