# HG changeset patch
# User wenzelm
# Date 1285341609 -7200
# Node ID b88a6bc371de9ecebccc97a7f0532a882d7d6219
# Parent  4ce5f79df87abdf55ad0303da484ef94c55ec382
tuned warning_color;

diff -r 4ce5f79df87a -r b88a6bc371de src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 24 17:12:09 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 24 17:20:09 2010 +0200
@@ -23,7 +23,7 @@
 
   val light_color = new Color(240, 240, 240)
   val regular_color = new Color(192, 192, 192)
-  val warning_color = new Color(255, 168, 0)
+  val warning_color = new Color(255, 140, 0)
   val error_color = new Color(178, 34, 34)
   val bad_color = new Color(255, 106, 106, 100)