--- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Jul 23 13:21:52 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Jul 23 14:53:21 2025 +0200
@@ -223,7 +223,7 @@
/* main content */
def tip_border(has_focus: Boolean): Unit = {
- val color = if (has_focus) GUI.default_background_color() else GUI.default_intermediate_color()
+ val color = if (has_focus) GUI.default_foreground_color() else GUI.default_intermediate_color()
pretty_tooltip.setBorder(new LineBorder(color))
pretty_tooltip.repaint()
}