# HG changeset patch
# User wenzelm
# Date 1554995272 -7200
# Node ID af4f723823d82c2acc6b0b128a2c7835c978b751
# Parent  b256f67e9d272a03f1fbd4247ef8c4dab93221e4
visible hairline for cursor, even on OpenJDK 11 (amending 2fd73a1a0937);

diff -r b256f67e9d27 -r af4f723823d8 src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Thu Apr 11 16:51:44 2019 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Thu Apr 11 17:07:52 2019 +0200
@@ -87,7 +87,7 @@
       new_styles(hidden) =
         new SyntaxStyle(hidden_color, null,
           GUI.transform_font(new Font(font0.getFamily, 0, 1),
-            AffineTransform.getScaleInstance(1.0, font0.getSize.toDouble)))
+            AffineTransform.getScaleInstance(2.0, font0.getSize.toDouble)))
       new_styles(control) =
         new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor,
           { val font_style =