# HG changeset patch
# User wenzelm
# Date 1677676935 -3600
# Node ID 3f13c6d476257f4dfc6676845d56d3c27461ae20
# Parent  9969b6aed223a766f0a5964ba76c11b11ad7e5c6
tuned signature;

diff -r 9969b6aed223 -r 3f13c6d47625 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 14:16:37 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 14:22:15 2023 +0100
@@ -98,11 +98,11 @@
   ) {
     def sessions_structure: Sessions.Structure = deps.sessions_structure
 
-    def apply(session: String): Build_Job.Session_Context =
+    def session_context(session: String): Build_Job.Session_Context =
       sessions.getOrElse(session, Build_Job.Session_Context.init(session))
 
     def old_command_timings(session: String): List[Properties.T] =
-      Properties.uncompress(apply(session).old_command_timings_blob, cache = store.cache)
+      Properties.uncompress(session_context(session).old_command_timings_blob, cache = store.cache)
 
     def do_store(session: String): Boolean =
       build_heap || Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session)