# HG changeset patch
# User wenzelm
# Date 1494001938 -7200
# Node ID 45b8446a8b52acfcbee6324c13095e17bbfb92f7
# Parent  7864aea16a87bdd61390ca4a638aafc37f1ddb4b
tuned;

diff -r 7864aea16a87 -r 45b8446a8b52 src/Pure/Admin/build_stats.scala
--- a/src/Pure/Admin/build_stats.scala	Fri May 05 18:15:53 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala	Fri May 05 18:32:18 2017 +0200
@@ -30,9 +30,8 @@
     val all_infos =
       Par_List.map((info: Jenkins.Job_Info) =>
         {
-          val t = info.timestamp / 1000
           val log_file = Build_Log.Log_File(info.log_filename.implode, Url.read(info.main_log))
-          (t, log_file.parse_build_info())
+          (info.date, log_file.parse_build_info())
         }, job_infos)
     val all_sessions =
       (Set.empty[String] /: all_infos)(
@@ -55,11 +54,11 @@
       Isabelle_System.with_tmp_file(session, "png") { data_file =>
         Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
           val data =
-            for { (t, info) <- all_infos if info.finished(session) }
+            for { (date, info) <- all_infos if info.finished(session) }
             yield {
               val timing1 = info.timing(session)
               val timing2 = info.ml_timing(session)
-              List(t.toString,
+              List(date.unix_epoch.toString,
                 timing1.elapsed.minutes,
                 timing1.cpu.minutes,
                 timing2.elapsed.minutes,
diff -r 7864aea16a87 -r 45b8446a8b52 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri May 05 18:15:53 2017 +0200
+++ b/src/Pure/General/date.scala	Fri May 05 18:32:18 2017 +0200
@@ -93,6 +93,7 @@
   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
   def to_utc: Date = to(ZoneId.of("UTC"))
 
+  def unix_epoch: Long = rep.toEpochSecond
   def instant: Instant = Instant.from(rep)
   def time: Time = Time.instant(instant)
   def timezone: ZoneId = rep.getZone