| changeset 63996 | 3f47fec9edfc |
| parent 63865 | ccac33e291b1 |
| child 64041 | fd454d9e97c4 |
--- a/src/Pure/Tools/build.scala Sun Oct 02 17:05:48 2016 +0200 +++ b/src/Pure/Tools/build.scala Sun Oct 02 19:36:57 2016 +0200 @@ -419,7 +419,7 @@ /** build with results **/ - class Results private [Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) + class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) { def sessions: Set[String] = results.keySet def cancelled(name: String): Boolean = results(name)._1.isEmpty