# HG changeset patch
# User wenzelm
# Date 1687005924 -7200
# Node ID c0ad1c0edd268ff28ebd46ac377d5d105037ab31
# Parent  43ed2541b7582f3b3bc39393e3ccca35f17b9846
tuned comments;

diff -r 43ed2541b758 -r c0ad1c0edd26 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Jun 17 13:09:11 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sat Jun 17 14:45:24 2023 +0200
@@ -144,7 +144,7 @@
   /** dynamic state **/
 
   case class Build(
-    build_uuid: String,
+    build_uuid: String,   // Database_Progress.context_uuid
     ml_platform: String,
     options: String,
     start: Date,
@@ -152,7 +152,7 @@
   )
 
   case class Worker(
-    worker_uuid: String,
+    worker_uuid: String,  // Database_Progress.agent_uuid
     build_uuid: String,
     start: Date,
     stamp: Date,
@@ -469,8 +469,8 @@
     /* workers */
 
     object Workers {
-      val worker_uuid = Generic.worker_uuid.make_primary_key  // progress.agent_uuid
-      val build_uuid = Generic.build_uuid  // progress.context_uuid
+      val worker_uuid = Generic.worker_uuid.make_primary_key
+      val build_uuid = Generic.build_uuid
       val start = SQL.Column.date("start")
       val stamp = SQL.Column.date("stamp")
       val stop = SQL.Column.date("stop")