# HG changeset patch
# User wenzelm
# Date 1677678563 -3600
# Node ID 080f76d138ed0783177fadc19144e850af39b745
# Parent  0c704aba71e37f4b7cbd6a70812d47b41414f43e
tuned signature (again);

diff -r 0c704aba71e3 -r 080f76d138ed src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 14:47:20 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 14:49:23 2023 +0100
@@ -43,7 +43,7 @@
     def init(name: String,
       deps: List[String],
       ancestors: List[String],
-      timeout: Time = Time.zero
+      timeout: Time
     ): Session_Context = new Session_Context(name, deps, ancestors, timeout, Time.zero, Bytes.empty)
 
     def load(
@@ -54,7 +54,7 @@
       store: Sessions.Store,
       progress: Progress = new Progress
     ): Session_Context = {
-      def default: Session_Context = init(name, deps, ancestors, timeout = timeout)
+      def default: Session_Context = init(name, deps, ancestors, timeout)
 
       store.try_open_database(name) match {
         case None => default