src/Tools/jEdit/src/jedit/document_view.scala
changeset 34794 a4a457e393a4
parent 34789 30528e68f774
child 34806 211ac6c4d4c9
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Dec 18 12:29:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Dec 18 15:00:08 2009 +0100
@@ -28,7 +28,7 @@
     command.status(doc) match {
       case Command.Status.UNPROCESSED => new Color(255, 228, 225)
       case Command.Status.FINISHED => new Color(234, 248, 255)
-      case Command.Status.FAILED => new Color(255, 106, 106)
+      case Command.Status.FAILED => new Color(255, 193, 193)
       case _ => Color.red
     }
   }