src/Pure/System/scala.scala
changeset 71865 3882df6a4a93
parent 71864 bfc120aa737a
child 71868 06ec50d9fc0a
equal deleted inserted replaced
71864:bfc120aa737a 71865:3882df6a4a93
    57       out.close
    57       out.close
    58 
    58 
    59       val Error = """(?s)^\S* error: (.*)$""".r
    59       val Error = """(?s)^\S* error: (.*)$""".r
    60       val errors =
    60       val errors =
    61         space_explode('\u0001', Library.strip_ansi_color(out.toString)).
    61         space_explode('\u0001', Library.strip_ansi_color(out.toString)).
    62           collect({ case Error(msg) => Word.capitalize(Library.trim_line(msg)) })
    62           collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
    63 
    63 
    64       if (!ok && errors.isEmpty) List("Error") else errors
    64       if (!ok && errors.isEmpty) List("Error") else errors
    65     }
    65     }
    66   }
    66   }
    67 
    67