# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737038290 -3600
# Node ID 691403dc5b92277faeaf9afb3a73e9543542b1d3
# Parent  1085eb118dc7c5c162eee5ac4a16c854e4e31953
tuned whitespace;

diff -r 1085eb118dc7 -r 691403dc5b92 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Jan 16 18:07:31 2025 +0100
+++ b/src/Pure/Build/build_schedule.scala	Thu Jan 16 15:38:10 2025 +0100
@@ -1261,7 +1261,7 @@
 
     def read_serial(db: SQL.Database, build_uuid: String = ""): Long =
       db.execute_query_statementO[Long](
-        Schedules.table.select(List(Schedules.serial.max), sql = 
+        Schedules.table.select(List(Schedules.serial.max), sql =
           SQL.where(if_proper(build_uuid, Schedules.build_uuid.equal(build_uuid)))),
           _.long(Schedules.serial)).getOrElse(0L)
 
@@ -1373,7 +1373,7 @@
         schedule.generator != old_schedule.generator ||
         schedule.start != old_schedule.start ||
         schedule.graph != old_schedule.graph
-      
+
       val schedule1 =
         if (changed) schedule.copy(serial = old_schedule.next_serial) else schedule
       if (schedule1.serial != schedule.serial) write_schedule(db, schedule1)