# HG changeset patch
# User wenzelm
# Date 1674418045 -3600
# Node ID 7b5b1789a34c23812c2b68ec748a1ca8a8a3f9cf
# Parent  164a21e5d5689ae11dbc6dd227f67e5c6e78547e
proper signature;

diff -r 164a21e5d568 -r 7b5b1789a34c src/Pure/Thy/sessions.scala
--- 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"),