workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read-only text;
authorwenzelm
Fri, 24 Nov 2023 19:42:53 +0100
changeset 79052 d5cf21ad8b47
parent 79051 c87e4a5a3823
child 79053 badb3da19ac6
workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read-only text;
src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Fri Nov 24 18:23:45 2023 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Fri Nov 24 19:42:53 2023 +0100
@@ -45,6 +45,7 @@
     text.columns = 60
     text.rows = 24
     text.font = GUI.copy_font((new Label).font)
+    text.caret.color = text.background
 
     private val scroll_text = new ScrollPane(text)