src/Pure/Admin/build_log.scala
changeset 79818 0c2a62a9f136
parent 79816 11fa48986f37
child 79819 141df3fb25bf
--- 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 {