Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust: avoid duplicate Socket.close;
  2. enable subpixel anti-aliasing by default, assuming that its 4 variants don't make a difference;
  3. updated to isabelle_fonts-20190210;
  4. recovered missing glyph;
  5. auto-hinting of original DejaVu fonts, but not Isabelle symbols;
Changeset 69799:18cb541a975f by wenzelm:
more robust: avoid duplicate Socket.close;
The file was modified src/Pure/General/socket_io.ML (diff)
Changeset 69798:f610115ca3d0 by wenzelm:
enable subpixel anti-aliasing by default, assuming that its 4 variants don't make a difference;
The file was modified src/Tools/jEdit/src/jEdit.props (diff)
Changeset 69797:7e5a7a11d5d1 by wenzelm:
updated to isabelle_fonts-20190210;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified Admin/isabelle_fonts/README (diff)
Changeset 69796:04c50000fad1 by wenzelm:
recovered missing glyph;
The file was modified src/Pure/Admin/build_fonts.scala (diff)
Changeset 69795:4791988fcbc4 by wenzelm:
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
The file was modified src/Pure/Admin/build_fonts.scala (diff)