# HG changeset patch # User Lars Hupel # Date 1474725414 -7200 # Node ID fbc2b562331bc90af667557cfda0008eb003c452 # Parent 9195600fcc7ceb0784e82cb9411680b16aabdef6 include generation time in statistics diff -r 9195600fcc7c -r fbc2b562331b Admin/jenkins/build/ci_build_stats.scala --- a/Admin/jenkins/build/ci_build_stats.scala Sat Sep 24 15:33:55 2016 +0200 +++ b/Admin/jenkins/build/ci_build_stats.scala Sat Sep 24 15:56:54 2016 +0200 @@ -1,14 +1,20 @@ object stats extends isabelle.Isabelle_Tool.Body { import isabelle._ + import java.time._ + import java.time.format.DateTimeFormatter + + + val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) val target_dir = Path.explode("stats") val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow") - val html_header = """ + val html_header = s""" Performance statistics from session build output +

Generated at $start_time

""" val html_footer = """