updated comments;
authorwenzelm
Sun Nov 05 15:50:26 2017 +0100 (17 months ago)
changeset 67011bab3208d8d37
parent 67010 cf56dd6f3ad1
child 67012 671decd2e627
updated comments;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Sun Nov 05 14:35:43 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sun Nov 05 15:50:26 2017 +0100
     1.3 @@ -124,14 +124,14 @@
     1.4  
     1.5      def - (name: String): Queue =
     1.6        new Queue(graph.del_node(name),
     1.7 -        order - name,  // FIXME scala-2.10.0 TreeSet problem!?
     1.8 +        order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
     1.9          command_timings)
    1.10  
    1.11      def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
    1.12      {
    1.13        val it = order.iterator.dropWhile(name =>
    1.14          skip(name)
    1.15 -          || !graph.defined(name)  // FIXME scala-2.10.0 TreeSet problem!?
    1.16 +          || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
    1.17            || !graph.is_minimal(name))
    1.18        if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
    1.19        else None