enable subpixel anti-aliasing by default, assuming that its 4 variants don't make a difference;
authorwenzelm
Sun Feb 10 19:07:53 2019 +0100 (2 months ago)
changeset 69798f610115ca3d0
parent 69797 7e5a7a11d5d1
child 69799 18cb541a975f
enable subpixel anti-aliasing by default, assuming that its 4 variants don't make a difference;
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Sun Feb 10 18:16:11 2019 +0100
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Sun Feb 10 19:07:53 2019 +0100
     1.3 @@ -303,7 +303,7 @@
     1.4  vfs.favorite.4=isabelle-export:
     1.5  vfs.favorite.5.type=1
     1.6  vfs.favorite.5=isabelle-session:
     1.7 -view.antiAlias=standard
     1.8 +view.antiAlias=subpixel HRGB
     1.9  view.blockCaret=true
    1.10  view.caretBlink=false
    1.11  view.docking.framework=PIDE