allow arbitrary info, e.g. for custom scheduler;
--- 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