src/Pure/Build/build_schedule.scala
changeset 80480 972f7a4cdc0e
parent 80476 59e088605d49
child 81340 30f7eb65d679
--- a/src/Pure/Build/build_schedule.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -549,7 +549,7 @@
           Schedule(build_uuid, generator, start, graph, serial)
         }
 
-      schedule(YXML.parse_body(File.read(file)))
+      schedule(YXML.parse_body(Bytes.read(file)))
     }
   }