# HG changeset patch
# User wenzelm
# Date 1509893426 -3600
# Node ID bab3208d8d37b005f4850502c0f70c6d28555307
# Parent  cf56dd6f3ad1ae793c4c92fa72764b8bb8b83ba9
updated comments;

diff -r cf56dd6f3ad1 -r bab3208d8d37 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Nov 05 14:35:43 2017 +0100
+++ b/src/Pure/Tools/build.scala	Sun Nov 05 15:50:26 2017 +0100
@@ -124,14 +124,14 @@
 
     def - (name: String): Queue =
       new Queue(graph.del_node(name),
-        order - name,  // FIXME scala-2.10.0 TreeSet problem!?
+        order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
         command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
     {
       val it = order.iterator.dropWhile(name =>
         skip(name)
-          || !graph.defined(name)  // FIXME scala-2.10.0 TreeSet problem!?
+          || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
           || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
       else None