read/write proper schedule date (amending 9da3019e1ee5);
authorFabian Huch <huch@in.tum.de>
Sat, 16 Mar 2024 21:22:02 +0100
changeset 79916 cfeb3a8f241d
parent 79915 40d2f9ce29fc
child 79918 87a04ce7e3c3
read/write proper schedule date (amending 9da3019e1ee5);
src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Mar 16 17:00:13 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Mar 16 21:22:02 2024 +0100
@@ -499,7 +499,7 @@
       import XML.Encode._
 
       def time: T[Time] = (time => long(time.ms))
-      def date: T[Date] = (date => long(date.unix_epoch))
+      def date: T[Date] = (date => time(date.time))
       def node_info: T[Node_Info] =
         (node_info => triple(string, option(int), list(int))(
           (node_info.hostname, node_info.numa_node, node_info.rel_cpus)))
@@ -519,7 +519,7 @@
       import XML.Decode._
 
       def time: T[Time] = { body => Time.ms(long(body)) }
-      def date: T[Date] = { body => Date(Time.ms(long(body))) }
+      def date: T[Date] = { body => Date(time(body)) }
       def node_info: T[Node_Info] =
         { body =>
           val (hostname, numa_node, rel_cpus) = triple(string, option(int), list(int))(body)