author | wenzelm |
Fri, 24 Nov 2023 19:42:53 +0100 | |
changeset 79052 | d5cf21ad8b47 |
parent 79051 | c87e4a5a3823 |
child 79053 | badb3da19ac6 |
--- 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)