| changeset 78164 | 5454bec8f5c6 |
| parent 78158 | 8b5a2e4b16d4 |
| child 78178 | a177f71dc79f |
--- a/src/Pure/Thy/export.scala Thu Jun 15 17:24:32 2023 +0200 +++ b/src/Pure/Thy/export.scala Thu Jun 15 17:29:29 2023 +0200 @@ -251,7 +251,7 @@ /* context for database access */ def open_database_context(store: Sessions.Store): Database_Context = { - val database_server = if (store.database_server) Some(store.open_database_server()) else None + val database_server = if (store.build_database_server) Some(store.open_database_server()) else None new Database_Context(store, database_server) }