# HG changeset patch
# User wenzelm
# Date 1709926145 -3600
# Node ID 0c2a62a9f1361fe3480a966e00d59f41dc9f48c3
# Parent  7308e402451ff080e08763c29431a704ac34cb39
more operations for Build_Log.Meta_Info: prefer explicit types;

diff -r 7308e402451f -r 0c2a62a9f136 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Mar 08 20:28:29 2024 +0100
+++ b/src/Pure/Admin/build_log.scala	Fri Mar 08 20:29:05 2024 +0100
@@ -280,6 +280,10 @@
 
     def get_date(c: SQL.Column): Option[Date] =
       get(c).map(Log_File.Date_Format.parse)
+
+    def get_build_host: Option[String] = get(Prop.build_host)
+    def get_build_start: Option[Date] = get_date(Prop.build_start)
+    def get_build_end: Option[Date] = get_date(Prop.build_end)
   }
 
   object Identify {
diff -r 7308e402451f -r 0c2a62a9f136 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Fri Mar 08 20:28:29 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Fri Mar 08 20:29:05 2024 +0100
@@ -42,7 +42,7 @@
       val measurements =
         for {
           (meta_info, build_info) <- build_history
-          build_host = meta_info.get(Build_Log.Prop.build_host)
+          build_host = meta_info.get_build_host
           (job_name, session_info) <- build_info.sessions.toList
           if build_info.finished_sessions.contains(job_name)
           hostname <- session_info.hostname.orElse(build_host).toList