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