# HG changeset patch
# User wenzelm
# Date 1708634522 -3600
# Node ID 5044f1d9196d0ea9c214a7255f359c608eeda524
# Parent  32ca3d1283de27ffaf39b1fe16f1742b44749a99
more thorough Store.clean_output (amending 1fa1b32b0379);

diff -r 32ca3d1283de -r 5044f1d9196d src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Thu Feb 22 21:28:55 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Thu Feb 22 21:42:02 2024 +0100
@@ -1111,7 +1111,7 @@
 
   def prepare(): Unit = {
     for (name <- build_context.clean_sessions) {
-      store.clean_output(_database_server, name, progress = progress)
+      store.clean_output(_database_server orElse _heaps_database, name, progress = progress)
     }
   }
 
diff -r 32ca3d1283de -r 5044f1d9196d src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Thu Feb 22 21:28:55 2024 +0100
+++ b/src/Pure/Build/store.scala	Thu Feb 22 21:42:02 2024 +0100
@@ -436,7 +436,9 @@
   ): Unit = {
     val relevant_db =
       database_server match {
-        case Some(db) => clean_session_info(db, name)
+        case Some(db) =>
+          ML_Heap.clean_entry(db, name)
+          clean_session_info(db, name)
         case None => false
       }