tuned warning_color;
authorwenzelm
Fri, 24 Sep 2010 17:20:09 +0200
changeset 39692 b88a6bc371de
parent 39691 4ce5f79df87a
child 39695 1906c0c77341
tuned warning_color;
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)