# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1702462451 -3600
# Node ID b88b6ed0633456a346f4537f1e8b2380fa12accd
# Parent  366a5ad2f2b337e8dfa8f5668c092583931bc134
read serial for schedules (amending 2039f360);

diff -r 366a5ad2f2b3 -r b88b6ed06334 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 {