# HG changeset patch
# User wenzelm
# Date 1753275201 -7200
# Node ID 89da4dcd1fa81204e31f77fec9a4c8fd60a7c72b
# Parent  9225b889f68ac54ccd08487ead0ab6f08de3f0a7
clarified colors, following d6a14ed060fb;

diff -r 9225b889f68a -r 89da4dcd1fa8 src/Tools/jEdit/src/pretty_tooltip.scala
--- 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()
   }