proper color;
authorwenzelm
Mon, 06 Mar 2017 11:39:41 +0100
changeset 65125 bdd58b74c4a4
parent 65124 759c64c39a6f
child 65126 45ccb8ee3d08
proper color;
src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 11:38:06 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 11:39:41 2017 +0100
@@ -452,7 +452,7 @@
     Rendering.warning_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), warning_message_color),
     Rendering.legacy_pri ->
-      (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), warning_message_color),
+      (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), legacy_message_color),
     Rendering.error_pri ->
       (JEdit_Lib.load_icon(options.string("gutter_error_icon")), error_message_color))