clarified permissions of build.db, following server.db;
authorwenzelm
Sun, 26 Feb 2023 20:52:14 +0100
changeset 77383 cb75171d8c9f
parent 77382 f4f9f987e7f2
child 77384 ef6673859c38
clarified permissions of build.db, following server.db;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Feb 26 20:27:11 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Feb 26 20:52:14 2023 +0100
@@ -517,7 +517,12 @@
   protected val database: Option[SQL.Database] =
     if (!build_options.bool("build_database") || true /*FIXME*/) None
     else if (store.database_server) Some(store.open_database_server())
-    else Some(SQLite.open_database(Build_Process.Data.database))
+    else {
+      val db = SQLite.open_database(Build_Process.Data.database)
+      try { Isabelle_System.chmod("600", Build_Process.Data.database) }
+      catch { case exn: Throwable => db.close(); throw exn }
+      Some(db)
+    }
 
   def close(): Unit = database.foreach(_.close())