changeset 77344 | de7eae726f8e |
parent 77343 | db479840d6ad |
child 77372 | 44fe9fe96130 |
--- a/src/Pure/Tools/build_process.scala Tue Feb 21 14:30:07 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Tue Feb 21 14:36:04 2023 +0100 @@ -152,7 +152,7 @@ /* dynamic state */ - case class Entry(name: String, deps: List[String]) { + case class Entry(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) { def is_ready: Boolean = deps.isEmpty def resolve(dep: String): Entry = if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this