tuned whitespace;
authorwenzelm
Wed, 15 Mar 2017 10:48:46 +0100
changeset 65253 85c0ac5c2589
parent 65252 8b776d12f6c0
child 65254 3075aa3b40bf
tuned whitespace;
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)
             }