# HG changeset patch
# User wenzelm
# Date 1700851373 -3600
# Node ID d5cf21ad8b4774219848fac744110470f5348afa
# Parent  c87e4a5a38231e2c633ed63dcdfa677d4482d9b2
workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read-only text;

diff -r c87e4a5a3823 -r d5cf21ad8b47 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)