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] ) {