# HG changeset patch
# User wenzelm
# Date 1488796781 -3600
# Node ID bdd58b74c4a453f21f8c48ac967b23612d85cdcd
# Parent  759c64c39a6f1a2dd28eeaad05cf4cbe9e9b6e14
proper color;

diff -r 759c64c39a6f -r bdd58b74c4a4 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))