# HG changeset patch
# User wenzelm
# Date 1489867035 -3600
# Node ID 944758d6462e15ffd7216887e90d8d011157daf9
# Parent  347ed6219dabaa0661ad60d862f4dd814a9341ac
tuned;

diff -r 347ed6219dab -r 944758d6462e src/Pure/Tools/build.scala
--- 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])