| changeset 78969 | 1b05c2b10c9f |
| parent 78968 | faa5af35fb65 |
| child 79020 | ef76705bf402 |
--- a/src/Pure/Tools/build_process.scala Fri Nov 10 14:07:36 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Fri Nov 10 14:42:07 2023 +0100 @@ -852,7 +852,7 @@ /* global resources with common close() operation */ - private val _database_server: Option[SQL.Database] = + protected val _database_server: Option[SQL.Database] = try { store.maybe_open_database_server(server = server) } catch { case exn: Throwable => close(); throw exn }