include generation time in statistics
authorLars Hupel <lars.hupel@mytum.de>
Sat, 24 Sep 2016 15:56:54 +0200
changeset 63943 fbc2b562331b
parent 63942 9195600fcc7c
child 63944 21eaff8c8fc9
include generation time in statistics
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 = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
+  val html_header = s"""<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
 <html>
 <head><title>Performance statistics from session build output</title></head>
 <body>
+  <p>Generated at $start_time</p>
 """
 
   val html_footer = """