# HG changeset patch
# User wenzelm
# Date 1677760006 -3600
# Node ID 5ecaf881b5634d5d0858c240a4a7ec961b2a5a06
# Parent  362bf802013ec67c4a2bf0dfe175a28a813ad4f3
clarified signature;

diff -r 362bf802013e -r 5ecaf881b563 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Mar 02 13:19:21 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Mar 02 13:26:46 2023 +0100
@@ -40,6 +40,13 @@
 
   def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name)
 
+  def start_session(
+    build_context: Build_Process.Context,
+    session_background: Sessions.Background,
+    input_shasum: SHA1.Shasum,
+    node_info: Node_Info
+  ): Session_Job = new Session_Job(build_context, session_background, input_shasum, node_info)
+
   object Session_Context {
     def load(
       name: String,
@@ -94,7 +101,7 @@
     override def toString: String = name
   }
 
-  class Session_Job(
+  class Session_Job private[Build_Job](
     build_context: Build_Process.Context,
     session_background: Sessions.Background,
     input_shasum: SHA1.Shasum,
diff -r 362bf802013e -r 5ecaf881b563 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Mar 02 13:19:21 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 02 13:26:46 2023 +0100
@@ -601,7 +601,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.Session_Job(
+        Build_Job.start_session(
           build_context, build_deps.background(session_name), input_shasum, node_info)
       state1.add_running(session_name, job)
     }