author | wenzelm |
Sat, 18 Mar 2017 20:57:15 +0100 | |
changeset 65314 | 944758d6462e |
parent 65313 | 347ed6219dab |
child 65315 | c7097ccbffb7 |
--- a/src/Pure/Tools/build.scala Sat Mar 18 20:51:42 2017 +0100 +++ b/src/Pure/Tools/build.scala Sat Mar 18 20:57:15 2017 +0100 @@ -104,7 +104,7 @@ } } - private final class Queue private( + private class Queue( graph: Graph[String, Sessions.Info], order: SortedSet[String], val command_timings: String => List[Properties.T])