# HG changeset patch
# User wenzelm
# Date 1687354878 -7200
# Node ID 40ae1cd71133be4f7350f830b222b3f83af2e0ba
# Parent  e9f96422f6072d4db5472ef4a244b55120a9ae88
proper clean_entry;

diff -r e9f96422f607 -r 40ae1cd71133 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Wed Jun 21 15:31:18 2023 +0200
+++ b/src/Pure/Thy/store.scala	Wed Jun 21 15:41:18 2023 +0200
@@ -312,11 +312,12 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
+    for (db <- maybe_open_heaps_database()) {
+      using(db)(ML_Heap.clean_entry(_, name))
+    }
+
     if (init) {
-      using(open_database(name, output = true)) { db =>
-        if (build_database_test && build_database_server) ML_Heap.clean_entry(db, name)
-        init_session_info(db, name)
-      }
+      using(open_database(name, output = true))(init_session_info(_, name))
     }
 
     if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None