--- a/src/Tools/jEdit/etc/options Thu Jun 24 06:06:32 2021 +0000
+++ b/src/Tools/jEdit/etc/options Fri Jun 25 12:32:56 2021 +0200
@@ -99,6 +99,8 @@
option warning_color : string = "FF8C00FF"
option legacy_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
+option ok_color : string = "000000FF"
+option failed_color : string = "B22222FF"
option writeln_message_color : string = "F0F0F0FF"
option information_message_color : string = "DCEAF3FF"
option tracing_message_color : string = "F0F8FFFF"