read serial for schedules (amending 2039f360);
authorFabian Huch <huch@in.tum.de>
Wed, 13 Dec 2023 11:14:11 +0100
changeset 79287 b88b6ed06334
parent 79286 366a5ad2f2b3
child 79288 92d2473687f0
read serial for schedules (amending 2039f360);
src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Mon Dec 18 22:49:33 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Wed Dec 13 11:14:11 2023 +0100
@@ -1041,7 +1041,8 @@
             val build_uuid = res.string(Schedules.build_uuid)
             val generator = res.string(Schedules.generator)
             val start = res.date(Schedules.start)
-            Schedule(build_uuid, generator, start, Graph.empty)
+            val serial = res.long(Schedules.serial)
+            Schedule(build_uuid, generator, start, Graph.empty, serial)
           })
 
       for (schedule <- schedules.sortBy(_.start)(Date.Ordering)) yield {