diff -r a45cce93529c -r 3b09ae9e40cb src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Mar 11 11:51:19 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Mar 11 12:41:53 2023 +0100
@@ -57,6 +57,7 @@
       name: String,
       deps: List[String],
       ancestors: List[String],
+      session_prefs: String,
       sources_shasum: SHA1.Shasum,
       timeout: Time,
       store: Sessions.Store,
@@ -64,7 +65,8 @@
     ): Session_Context = {
       def default: Session_Context =
         Session_Context(
-          name, deps, ancestors, sources_shasum, timeout, Time.zero, Bytes.empty, build_uuid)
+          name, deps, ancestors, session_prefs, sources_shasum, timeout,
+          Time.zero, Bytes.empty, build_uuid)
 
       store.try_open_database(name) match {
         case None => default
@@ -83,7 +85,8 @@
                 case _ => Time.zero
               }
             new Session_Context(
-              name, deps, ancestors, sources_shasum, timeout, elapsed, command_timings, build_uuid)
+              name, deps, ancestors, session_prefs, sources_shasum, timeout,
+              elapsed, command_timings, build_uuid)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
@@ -99,6 +102,7 @@
     name: String,
     deps: List[String],
     ancestors: List[String],
+    session_prefs: String,
     sources_shasum: SHA1.Shasum,
     timeout: Time,
     old_time: Time,