src/Pure/Tools/build.scala
changeset 62406 b5b8fb87447a
parent 62405 d653532762e4
child 62409 e391528eff3b
     1.1 --- a/src/Pure/Tools/build.scala	Thu Feb 25 00:27:57 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Feb 25 00:35:17 2016 +0100
     1.3 @@ -738,8 +738,10 @@
     1.4    {
     1.5      def sessions: Set[String] = results.keySet
     1.6      def cancelled(name: String): Boolean = results(name).isEmpty
     1.7 -    def process_result(name: String): Process_Result = results(name).getOrElse(Process_Result(1))
     1.8 +    def apply(name: String): Process_Result = results(name).getOrElse(Process_Result(1))
     1.9      val rc = (0 /: results.iterator.map({ case (_, Some(r)) => r.rc case (_, None) => 1 }))(_ max _)
    1.10 +
    1.11 +    override def toString: String = rc.toString
    1.12    }
    1.13  
    1.14    def build_results(
    1.15 @@ -1026,7 +1028,7 @@
    1.16        val unfinished =
    1.17          (for {
    1.18            name <- results.sessions.iterator
    1.19 -          if !results.process_result(name).ok
    1.20 +          if !results(name).ok
    1.21           } yield name).toList.sorted
    1.22        progress.echo("Unfinished session(s): " + commas(unfinished))
    1.23      }