# HG changeset patch
# User wenzelm
# Date 1677694683 -3600
# Node ID 5b9848b1ba30ff05fa9ea6007556f0ccddf9ee97
# Parent  e72b1f5fd88df2eb34407b5e4874a104cb75b753
tuned signature;

diff -r e72b1f5fd88d -r 5b9848b1ba30 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 19:13:19 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 19:18:03 2023 +0100
@@ -91,7 +91,7 @@
     override def toString: String = name
   }
 
-  class Build_Session(
+  class Session_Job(
     progress: Progress,
     verbose: Boolean,
     session_background: Sessions.Background,
diff -r e72b1f5fd88d -r 5b9848b1ba30 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 19:13:19 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 19:18:03 2023 +0100
@@ -628,7 +628,7 @@
           val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
           val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
           val job =
-            new Build_Job.Build_Session(progress, verbose, session_background, session_heaps,
+            new Build_Job.Session_Job(progress, verbose, session_background, session_heaps,
               store, do_store, resources, build_context.session_setup,
               build_deps.sources_shasum(session_name), input_heaps, node_info)
           _state = state1.add_running(session_name, job)