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))) } }