remove old build before generating schedule;
authorFabian Huch <huch@in.tum.de>
Sat, 16 Mar 2024 10:02:16 +0100
changeset 79908 c50c15bd304b
parent 79907 01652fac1039
child 79909 18969501a13e
remove old build before generating schedule;
src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Mar 16 09:58:23 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Mar 16 10:02:16 2024 +0100
@@ -1375,6 +1375,8 @@
     session_setup: (String, Session) => Unit = (_, _) => (),
     cache: Term.Cache = Term.Cache.make()
   ): Schedule = {
+    Build.build_process(options, build_cluster = true, remove_builds = true)
+
     val store =
       Build_Engine.build_store(options, build_cluster = build_hosts.nonEmpty, cache = cache)
     val log_store = Build_Log.store(options, cache = cache)