author | wenzelm |
Thu, 22 Sep 2022 16:17:02 +0200 | |
changeset 76202 | d535db35388e |
parent 76201 | 9d1819c28f67 |
child 76203 | 258056f533ce |
--- a/src/Pure/Tools/build.scala Thu Sep 22 14:14:45 2022 +0200 +++ b/src/Pure/Tools/build.scala Thu Sep 22 16:17:02 2022 +0200 @@ -149,8 +149,7 @@ foldLeft(Process_Result.RC.ok)(_ max _) def ok: Boolean = rc == Process_Result.RC.ok - def unfinished: List[String] = - sessions.iterator.filterNot(name => !apply(name).ok).toList.sorted + def unfinished: List[String] = sessions.iterator.filterNot(apply(_).ok).toList.sorted override def toString: String = rc.toString }