# HG changeset patch # User wenzelm # Date 1677699422 -3600 # Node ID 7a52ba76aa9e0176f2342fdbe843fc7748c36443 # Parent 403748b23f13eb9d7ae4c50cdaa3ab86d78c860d tuned signature; diff -r 403748b23f13 -r 7a52ba76aa9e src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Wed Mar 01 20:21:09 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Wed Mar 01 20:37:02 2023 +0100 @@ -103,9 +103,7 @@ ) { def sessions_structure: Sessions.Structure = build_deps.sessions_structure - def session_context(session: String): Build_Job.Session_Context = sessions(session) - - def sources_shasum(session: String): SHA1.Shasum = session_context(session).sources_shasum + def sources_shasum(session: String): SHA1.Shasum = sessions(session).sources_shasum def old_command_timings(session: String): List[Properties.T] = sessions.get(session) match { @@ -555,7 +553,7 @@ protected def start_job(session_name: String): Unit = { val ancestor_results = synchronized { - _state.get_results(build_context.session_context(session_name).ancestors) + _state.get_results(build_context.sessions(session_name).ancestors) } val input_heaps = if (ancestor_results.isEmpty) {