src/Pure/Tools/build.scala
changeset 73344 f5c147654661
parent 73340 0ffcad1f6130
child 73359 d8a0e996614b
--- a/src/Pure/Tools/build.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/Tools/build.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -142,7 +142,7 @@
         skip(name)
           || !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))) }
+      if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
       else None
     }
   }