# HG changeset patch
# User wenzelm
# Date 1670927392 -3600
# Node ID 833bae85ac2d63866295e683fd1df908fe317f46
# Parent  76ee2762c69eb1934fdc712d285b975310298fa1
tuned;

diff -r 76ee2762c69e -r 833bae85ac2d src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Dec 13 11:27:51 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Dec 13 11:29:52 2022 +0100
@@ -688,17 +688,17 @@
 
       val root_infos = {
         var chapter = UNSORTED
-        val info_roots = new mutable.ListBuffer[Info]
+        val root_infos = new mutable.ListBuffer[Info]
         for (root <- roots) {
           root.entries.foreach {
             case entry: Chapter_Entry => chapter = entry.name
             case entry: Session_Entry =>
-              info_roots += Info.make(chapter_defs, options, root.select, root.dir, chapter, entry)
+              root_infos += Info.make(chapter_defs, options, root.select, root.dir, chapter, entry)
             case _ =>
           }
           chapter = UNSORTED
         }
-        info_roots.toList
+        root_infos.toList
       }
 
       val info_graph =