--- a/src/Tools/jEdit/etc/options Fri May 16 12:41:42 2025 +0200
+++ b/src/Tools/jEdit/etc/options Fri May 16 20:31:52 2025 +0200
@@ -93,7 +93,6 @@
option running_color : string = "610061FF" for color_dialog
option running1_color : string = "61006164" for color_dialog
option bullet_color : string = "000000FF" for color_dialog
-option tooltip_color : string = "FFFFE9FF" for color_dialog
option writeln_color : string = "C0C0C0FF" for color_dialog
option information_color : string = "C1DFEEFF" for color_dialog
option warning_color : string = "FF8C00FF" for color_dialog
@@ -162,7 +161,6 @@
option running_color_dark : string = "7FBFFF00" for color_dialog
option running1_color_dark : string = "590259FF" for color_dialog
option bullet_color_dark : string = "EAEAEAFF" for color_dialog
-option tooltip_color_dark : string = "2B2B2BFF" for color_dialog
option writeln_color_dark : string = "9C9C9CFF" for color_dialog
option information_color_dark : string = "77B800FF" for color_dialog
option warning_color_dark : string = "FF8C00FF" for color_dialog