--- a/src/Pure/Thy/store.scala Wed Jun 21 11:15:04 2023 +0200
+++ b/src/Pure/Thy/store.scala Wed Jun 21 11:42:11 2023 +0200
@@ -312,7 +312,12 @@
path = dir + file if path.is_file
} yield path.file.delete
- if (init) using(open_database(name, output = true))(init_session_info(_, 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)
+ }
+ }
if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
}