changeset 56372 | fadb0fef09d7 |
parent 56208 | 06cc31dff138 |
child 56662 | f373fb77e0a4 |
--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Apr 02 18:35:07 2014 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Apr 02 20:22:12 2014 +0200 @@ -182,7 +182,7 @@ val iterator = restriction match { case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name))) - case None => snapshot.version.nodes.entries + case None => snapshot.version.nodes.iterator } val nodes_timing1 = (nodes_timing /: iterator)({ case (timing1, (name, node)) =>