# HG changeset patch
# User wenzelm
# Date 1456356917 -3600
# Node ID b5b8fb87447ae08ca3c261317618514fac6eefec
# Parent  d653532762e4670725b8d71713467488e72f56f0
tuned signature;

diff -r d653532762e4 -r b5b8fb87447a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Feb 25 00:27:57 2016 +0100
+++ b/src/Pure/Tools/build.scala	Thu Feb 25 00:35:17 2016 +0100
@@ -738,8 +738,10 @@
   {
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = results(name).isEmpty
-    def process_result(name: String): Process_Result = results(name).getOrElse(Process_Result(1))
+    def apply(name: String): Process_Result = results(name).getOrElse(Process_Result(1))
     val rc = (0 /: results.iterator.map({ case (_, Some(r)) => r.rc case (_, None) => 1 }))(_ max _)
+
+    override def toString: String = rc.toString
   }
 
   def build_results(
@@ -1026,7 +1028,7 @@
       val unfinished =
         (for {
           name <- results.sessions.iterator
-          if !results.process_result(name).ok
+          if !results(name).ok
          } yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }