# HG changeset patch
# User wenzelm
# Date 1677847186 -3600
# Node ID 2d5529f561243cc7b03084d616c0b7ab5089ba53
# Parent  8a28ab58d155e20b46bc55dab0c3e0b9ff0f5a9b
tuned signature;

diff -r 8a28ab58d155 -r 2d5529f56124 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Mar 03 11:25:29 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Mar 03 13:39:46 2023 +0100
@@ -111,13 +111,13 @@
     def session_name: String = session_background.session_name
     def job_name: String = session_name
 
-    val info: Sessions.Info = session_background.sessions_structure(session_name)
-    val options: Options = Host.process_policy_options(info.options, node_info.numa_node)
+    private val info: Sessions.Info = session_background.sessions_structure(session_name)
+    private val options: Options = Host.process_policy_options(info.options, node_info.numa_node)
 
-    val session_sources: Sessions.Sources =
+    private val session_sources =
       Sessions.Sources.load(session_background.base, cache = store.cache.compress)
 
-    val store_heap = build_context.store_heap(session_name)
+    private val store_heap = build_context.store_heap(session_name)
 
     private val future_result: Future[(Process_Result, SHA1.Shasum)] =
       Future.thread("build", uninterruptible = true) {