# 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