--- a/src/Pure/Build/build.scala Fri Mar 08 13:05:01 2024 +0100
+++ b/src/Pure/Build/build.scala Fri Mar 08 14:14:05 2024 +0100
@@ -40,6 +40,7 @@
no_build: Boolean = false,
session_setup: (String, Session) => Unit = (_, _) => (),
build_uuid: String = UUID.random_string(),
+ build_start: Option[Date] = None,
jobs: Int = 0,
master: Boolean = false
) {
@@ -632,7 +633,8 @@
val build_context =
Context(store, build_deps, engine = engine, afp_root = afp_root,
hostname = hostname(build_options), numa_shuffling = numa_shuffling,
- build_uuid = build_master.build_uuid, jobs = max_jobs.getOrElse(1))
+ build_uuid = build_master.build_uuid, build_start = Some(build_master.start),
+ jobs = max_jobs.getOrElse(1))
engine.run_build_process(build_context, progress, server)
}
--- a/src/Pure/Build/build_process.scala Fri Mar 08 13:05:01 2024 +0100
+++ b/src/Pure/Build/build_process.scala Fri Mar 08 14:14:05 2024 +0100
@@ -354,14 +354,15 @@
db: SQL.Database,
build_uuid: String,
ml_platform: String,
- options: String
+ options: String,
+ start: Date
): Unit = {
db.execute_statement(Base.table.insert(), body =
{ stmt =>
stmt.string(1) = build_uuid
stmt.string(2) = ml_platform
stmt.string(3) = options
- stmt.date(4) = db.now()
+ stmt.date(4) = start
stmt.date(5) = None
})
}
@@ -914,6 +915,8 @@
}
}
+ protected val build_start: Date = build_context.build_start getOrElse progress.now()
+
protected val log: Logger = Logger.make_system_log(progress, build_options)
protected def open_build_cluster(): Build_Cluster =
@@ -1082,7 +1085,7 @@
protected final def start_build(): Unit = synchronized_database("Build_Process.start_build") {
for (db <- _build_database) {
Build_Process.private_data.start_build(db, build_uuid, build_context.ml_platform,
- build_context.sessions_structure.session_prefs)
+ build_context.sessions_structure.session_prefs, build_start)
}
}