src/Pure/Tools/build_process.scala
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