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 } }