src/Pure/Tools/build_process.scala
changeset 77254 8d34f53871b4
parent 77249 f3f1b7ad1d0d
child 77255 b810e99b5afb
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 22:36:13 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 22:59:23 2023 +0100
@@ -110,11 +110,12 @@
             }
         }
 
-      new Context(sessions, ordering)
+      new Context(sessions_structure, sessions, ordering)
     }
   }
 
   final class Context private(
+    val sessions_structure: Sessions.Structure,
     sessions: Map[String, Session_Context],
     val ordering: Ordering[String]
   ) {