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 {