# HG changeset patch
# User wenzelm
# Date 1687871447 -7200
# Node ID af6c493b0441426075500c3ec5770ceb2eca229c
# Parent  13edc16bc14c94ccc02529b0781bf49363e84804
tuned;

diff -r 13edc16bc14c -r af6c493b0441 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Tue Jun 27 14:50:48 2023 +0200
+++ b/src/Pure/Thy/store.scala	Tue Jun 27 15:10:47 2023 +0200
@@ -305,12 +305,16 @@
   def clean_output(
     database_server: Option[SQL.Database],
     name: String,
-    init: Boolean = false
+    session_init: Boolean = false
   ): Option[Boolean] = {
     val relevant_db =
       database_server match {
-        case Some(db) => clean_session_info(db, name)
-        case None => false
+        case Some(db) =>
+          ML_Heap.clean_entry(db, name)
+          clean_session_info(db, name)
+        case None =>
+          if (session_init) using(open_database(name, output = true))(clean_session_info(_, name))
+          false
       }
 
     val del =
@@ -321,12 +325,6 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
-    database_server.foreach(ML_Heap.clean_entry(_, name))
-
-    if (init) {
-      using(open_database(name, output = true))(clean_session_info(_, name))
-    }
-
     if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
   }
 
diff -r 13edc16bc14c -r af6c493b0441 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Jun 27 14:50:48 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Tue Jun 27 15:10:47 2023 +0200
@@ -952,7 +952,7 @@
         (if (store_heap) "Building " else "Running ") + session_name +
           if_proper(node_info.numa_node, " on " + node_info) + " ...")
 
-      store.clean_output(_database_server, session_name, init = true)
+      store.clean_output(_database_server, session_name, session_init = true)
 
       val build =
         Build_Job.start_session(build_context, progress, log, _database_server,