# HG changeset patch
# User wenzelm
# Date 1677752750 -3600
# Node ID 50488bcd99f6c4410aced43f4c1807262160ae46
# Parent  38503d9ff2e5676f51b1e1fecf6cd254bd444dd6
tuned;

diff -r 38503d9ff2e5 -r 50488bcd99f6 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
           }
         }