# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700769499 -3600
# Node ID 49e8b031e0cb3044c28b42447287483da6ea6c69
# Parent  6bada416ba550e8c2780cb784a6f0354874b0135
tuned;

diff -r 6bada416ba55 -r 49e8b031e0cb src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 23 20:53:58 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 23 20:58:19 2023 +0100
@@ -13,14 +13,6 @@
 object Build_Schedule {
   val engine_name = "build_schedule"
 
-  object Config {
-    def from_job(job: Build_Process.Job): Config = Config(job.name, job.node_info)
-  }
-
-  case class Config(job_name: String, node_info: Node_Info) {
-    def job_of(start_time: Time): Build_Process.Job =
-      Build_Process.Job(job_name, "", "", node_info, Date(start_time), None)
-  }
 
   /* organized historic timing information (extracted from build logs) */
 
@@ -260,7 +252,16 @@
   }
 
 
-  /* offline tracking of resource allocations */
+  /* offline tracking of job configurations and resource allocations */
+
+  object Config {
+    def from_job(job: Build_Process.Job): Config = Config(job.name, job.node_info)
+  }
+
+  case class Config(job_name: String, node_info: Node_Info) {
+    def job_of(start_time: Time): Build_Process.Job =
+      Build_Process.Job(job_name, "", "", node_info, Date(start_time), None)
+  }
 
   case class Resources(
     host_infos: Host_Infos,