# HG changeset patch
# User wenzelm
# Date 1677441134 -3600
# Node ID cb75171d8c9ff5dede164873770cd4b8151e4625
# Parent  f4f9f987e7f2c2589417661b4d8b8563444c0d38
clarified permissions of build.db, following server.db;

diff -r f4f9f987e7f2 -r cb75171d8c9f 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())