src/Pure/Tools/server.scala
changeset 78163 c6d4b1a00ad7
parent 78162 41a87c4ea765
child 78166 70041580b81e
--- a/src/Pure/Tools/server.scala	Thu Jun 15 17:03:48 2023 +0200
+++ b/src/Pure/Tools/server.scala	Thu Jun 15 17:24:32 2023 +0200
@@ -397,9 +397,8 @@
     existing_server: Boolean = false,
     log: Logger = No_Logger
   ): (Info, Option[Server]) = {
-    using(SQLite.open_database(Data.database)) { db =>
+    using(SQLite.open_database(Data.database, restrict = true)) { db =>
       db.transaction {
-        File.restrict(Data.database)
         Data.tables.create_lock(db)
         list(db).filterNot(_.active).foreach(server_info =>
           db.execute_statement(Data.table.delete(sql = Data.name.where_equal(server_info.name))))