author | wenzelm |
Sat, 17 Dec 2022 17:28:05 +0100 | |
changeset 76667 | fa81f218c96e |
parent 76666 | 981801179bc5 |
child 76668 | dd03c91cda43 |
--- a/src/Pure/Tools/build_job.scala Sat Dec 17 17:02:09 2022 +0100 +++ b/src/Pure/Tools/build_job.scala Sat Dec 17 17:28:05 2022 +0100 @@ -254,7 +254,6 @@ private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") - val base = deps(parent) val result_base = deps(session_name) val env =