# HG changeset patch
# User wenzelm
# Date 1687951853 -7200
# Node ID 1ba48d4020057f339fe59b247e7036faf3522c6f
# Parent  73be8ec887219b620db7a77dad3734590e571a44
proper session_init *after* deleting db files (amending af6c493b0441);

diff -r 73be8ec88721 -r 1ba48d402005 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Wed Jun 28 12:39:43 2023 +0200
+++ b/src/Pure/Thy/store.scala	Wed Jun 28 13:30:53 2023 +0200
@@ -313,9 +313,7 @@
         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
+        case None => false
       }
 
     val del =
@@ -326,6 +324,10 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
+    if (database_server.isEmpty && session_init) {
+      using(open_database(name, output = true))(clean_session_info(_, name))
+    }
+
     if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
   }