# HG changeset patch
# User wenzelm
# Date 1677681818 -3600
# Node ID 167b5095ba14100087032395aac88eb9fbdc5e92
# Parent  25a94a1b09da764ea11f0e0d03448556a01719de
tuned signature (again);

diff -r 25a94a1b09da -r 167b5095ba14 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 15:41:56 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 15:43:38 2023 +0100
@@ -40,12 +40,6 @@
   /* build session */
 
   object Session_Context {
-    def init(name: String,
-      deps: List[String],
-      ancestors: List[String],
-      timeout: Time
-    ): Session_Context = new Session_Context(name, deps, ancestors, timeout, Time.zero, Bytes.empty)
-
     def load(
       name: String,
       deps: List[String],
@@ -54,7 +48,8 @@
       store: Sessions.Store,
       progress: Progress = new Progress
     ): Session_Context = {
-      def default: Session_Context = init(name, deps, ancestors, timeout)
+      def default: Session_Context =
+        new Session_Context(name, deps, ancestors, timeout, Time.zero, Bytes.empty)
 
       store.try_open_database(name) match {
         case None => default