# HG changeset patch
# User wenzelm
# Date 1677701068 -3600
# Node ID b474d39ddfeefb8e2522cb22838f98e1c1e745b3
# Parent  a553e419e9dc445c05daeb076f3fb7b07f4f377b
tuned signature;

diff -r a553e419e9dc -r b474d39ddfee src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 20:59:37 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 21:04:28 2023 +0100
@@ -103,18 +103,18 @@
   ) {
     def sessions_structure: Sessions.Structure = build_deps.sessions_structure
 
-    def sources_shasum(session: String): SHA1.Shasum = sessions(session).sources_shasum
+    def sources_shasum(name: String): SHA1.Shasum = sessions(name).sources_shasum
 
-    def old_command_timings(session: String): List[Properties.T] =
-      sessions.get(session) match {
+    def old_command_timings(name: String): List[Properties.T] =
+      sessions.get(name) match {
         case Some(session_context) =>
           Properties.uncompress(session_context.old_command_timings_blob, cache = store.cache)
         case None => Nil
       }
 
-    def do_store(session: String): Boolean =
-      build_heap || Sessions.is_pure(session) ||
-      sessions.valuesIterator.exists(_.ancestors.contains(session))
+    def do_store(name: String): Boolean =
+      build_heap || Sessions.is_pure(name) ||
+      sessions.valuesIterator.exists(_.ancestors.contains(name))
   }