tuned;
authorwenzelm
Thu, 02 Mar 2023 11:25:50 +0100
changeset 77471 50488bcd99f6
parent 77470 38503d9ff2e5
child 77472 a073ac3f3b56
tuned;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Mar 02 11:19:41 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 02 11:25:50 2023 +0100
@@ -1484,13 +1484,13 @@
         database_server && {
           try_open_database(name) match {
             case Some(db) =>
-              try {
+              using(db) { db =>
                 db.transaction {
                   val relevant_db = session_info_defined(db, name)
                   init_session_info(db, name)
                   relevant_db
                 }
-              } finally { db.close() }
+              }
             case None => false
           }
         }