# HG changeset patch
# User wenzelm
# Date 1590224044 -7200
# Node ID 3882df6a4a931907af957b3892ab855f3b9a82ba
# Parent  bfc120aa737a562e54097b02a485c433ad8e6504
tuned message;

diff -r bfc120aa737a -r 3882df6a4a93 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Fri May 22 15:53:47 2020 +0200
+++ b/src/Pure/System/scala.scala	Sat May 23 10:54:04 2020 +0200
@@ -59,7 +59,7 @@
       val Error = """(?s)^\S* error: (.*)$""".r
       val errors =
         space_explode('\u0001', Library.strip_ansi_color(out.toString)).
-          collect({ case Error(msg) => Word.capitalize(Library.trim_line(msg)) })
+          collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
 
       if (!ok && errors.isEmpty) List("Error") else errors
     }