1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Dec 18 12:29:30 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Dec 18 15:00:08 2009 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4      command.status(doc) match {
     1.5        case Command.Status.UNPROCESSED => new Color(255, 228, 225)
     1.6        case Command.Status.FINISHED => new Color(234, 248, 255)
     1.7 -      case Command.Status.FAILED => new Color(255, 106, 106)
     1.8 +      case Command.Status.FAILED => new Color(255, 193, 193)
     1.9        case _ => Color.red
    1.10      }
    1.11    }