proper session_init *after* deleting db files (amending af6c493b0441);
authorwenzelm
Wed, 28 Jun 2023 13:30:53 +0200
changeset 78227 1ba48d402005
parent 78226 73be8ec88721
child 78228 67e836ce3f04
proper session_init *after* deleting db files (amending af6c493b0441);
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
   }