# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1724757130 -7200
# Node ID d6417e967a7cda3a812c943a92215d31304d0d19
# Parent  a1b3abc629afc08787306eb30c6f945bdf3ce0fe
more robust: clean up unfinished jobs on init, e.g. if build_manager process was forcefully terminated;

diff -r a1b3abc629af -r d6417e967a7c src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Aug 27 12:57:49 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Aug 27 13:12:10 2024 +0200
@@ -1019,7 +1019,20 @@
 
     override def stopped(state: Runner.State): Boolean = progress.stopped && state.is_empty
 
-    def init: Runner.State = Runner.State.init(store.options)
+    def init: Runner.State = synchronized_database("init") {
+      for ((name, job) <- _state.running) {
+        echo("Cleaned up job " + job.uuid)
+
+        val report = store.report(job.kind, job.id)
+
+        _state = _state
+          .remove_running(job.name)
+          .add_finished(report.result(Some(job.uuid), job.user))
+      }
+
+      Runner.State.init(store.options)
+    }
+
     def loop_body(state: Runner.State): Runner.State = {
       val state1 =
         if (progress.stopped) state