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