author | wenzelm |
Sun, 22 Jan 2023 21:07:25 +0100 | |
changeset 77038 | 7b5b1789a34c |
parent 77037 | 164a21e5d568 |
child 77039 | 2f09dc0e6dda |
--- a/src/Pure/Thy/sessions.scala Sun Jan 22 20:40:51 2023 +0100 +++ b/src/Pure/Thy/sessions.scala Sun Jan 22 21:07:25 2023 +0100 @@ -1419,7 +1419,7 @@ def database_server: Boolean = options.bool("build_database_server") - def open_database_server(): SQL.Database = + def open_database_server(): PostgreSQL.Database = PostgreSQL.open_database( user = options.string("build_database_user"), password = options.string("build_database_password"),