# HG changeset patch
# User wenzelm
# Date 1649497297 -7200
# Node ID 6c3190da97012d864940804a614d75e93526681e
# Parent  3c710067b178ebadd6dea41c0f63970166edf632
proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;

diff -r 3c710067b178 -r 6c3190da9701 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Fri Apr 08 16:42:52 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Sat Apr 09 11:41:37 2022 +0200
@@ -235,7 +235,7 @@
   }
 
   private def count_crossings(graph: Graph, levels: List[Level]): Int =
-    levels.iterator.sliding(2).map {
+    levels.iterator.sliding(2).map(_.toList).map {
       case List(top, bot) =>
         top.iterator.zipWithIndex.map {
           case (outer_parent, outer_parent_index) =>