tuned whitespace;
authorwenzelm
Wed Mar 15 10:48:46 2017 +0100 (2017-03-15)
changeset 6525385c0ac5c2589
parent 65252 8b776d12f6c0
child 65254 3075aa3b40bf
tuned whitespace;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Wed Mar 15 10:43:54 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 15 10:48:46 2017 +0100
     1.3 @@ -250,7 +250,9 @@
     1.4      def cancelled(name: String): Boolean = results(name)._1.isEmpty
     1.5      def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     1.6      def info(name: String): Sessions.Info = results(name)._2
     1.7 -    val rc = (0 /: results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
     1.8 +    val rc =
     1.9 +      (0 /: results.iterator.map(
    1.10 +        { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
    1.11      def ok: Boolean = rc == 0
    1.12  
    1.13      override def toString: String = rc.toString
    1.14 @@ -507,7 +509,8 @@
    1.15                  }
    1.16                  else {
    1.17                    progress.echo(name + " CANCELLED")
    1.18 -                  loop(pending - name, running, results + (name -> Result(false, heap_stamp, None, info)))
    1.19 +                  loop(pending - name, running,
    1.20 +                    results + (name -> Result(false, heap_stamp, None, info)))
    1.21                  }
    1.22                case None => sleep(); loop(pending, running, results)
    1.23              }