# HG changeset patch
# User wenzelm
# Date 1676986564 -3600
# Node ID de7eae726f8ef846c47c0ac8b5af3c9f21b0787f
# Parent  db479840d6add9551fcba5ca3dd4eb994fb57326
allow arbitrary info, e.g. for custom scheduler;

diff -r db479840d6ad -r de7eae726f8e src/Pure/Tools/build_process.scala
--- 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