author | wenzelm |
Fri, 18 Dec 2009 15:00:08 +0100 | |
changeset 34794 | a4a457e393a4 |
parent 34793 | 3975494a4d8f |
child 34795 | c97335b7e8c3 |
--- 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 } }