--- a/src/Pure/Tools/build_job.scala Tue Mar 14 10:16:45 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Mar 14 10:27:17 2023 +0100
@@ -11,7 +11,6 @@
trait Build_Job {
- def node_info: Host.Node_Info
def cancel(): Unit = ()
def is_finished: Boolean = false
def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum)
@@ -103,7 +102,7 @@
log: Logger,
session_background: Sessions.Background,
input_shasum: SHA1.Shasum,
- override val node_info: Host.Node_Info
+ node_info: Host.Node_Info
) extends Build_Job {
private val store = build_context.store