# HG changeset patch
# User wenzelm
# Date 1489571326 -3600
# Node ID 85c0ac5c2589405d3fc2a3dd8879d00ab78c7524
# Parent  8b776d12f6c05c6eff81017918b14646356346c1
tuned whitespace;

diff -r 8b776d12f6c0 -r 85c0ac5c2589 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 15 10:43:54 2017 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 15 10:48:46 2017 +0100
@@ -250,7 +250,9 @@
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def info(name: String): Sessions.Info = results(name)._2
-    val rc = (0 /: results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
+    val rc =
+      (0 /: results.iterator.map(
+        { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
     def ok: Boolean = rc == 0
 
     override def toString: String = rc.toString
@@ -507,7 +509,8 @@
                 }
                 else {
                   progress.echo(name + " CANCELLED")
-                  loop(pending - name, running, results + (name -> Result(false, heap_stamp, None, info)))
+                  loop(pending - name, running,
+                    results + (name -> Result(false, heap_stamp, None, info)))
                 }
               case None => sleep(); loop(pending, running, results)
             }