tuned signature;
authorwenzelm
Wed, 01 Mar 2023 14:22:15 +0100
changeset 77443 3f13c6d47625
parent 77442 9969b6aed223
child 77444 0c704aba71e3
tuned signature;
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)