# HG changeset patch # User wenzelm # Date 1689930350 -7200 # Node ID dcaf6f33d94d686805a48f5160a05778e200e59c # Parent fd24f380b588af601eee688b9efc202fac4a449e tuned output; diff -r fd24f380b588 -r dcaf6f33d94d src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Fri Jul 21 10:56:11 2023 +0200 +++ b/src/Pure/General/sql.scala Fri Jul 21 11:05:50 2023 +0200 @@ -647,7 +647,8 @@ val name = proper_string(database) getOrElse user val url = "jdbc:postgresql://" + server.host + ":" + server.port + "/" + name val ssh = server.ssh_system.ssh_session - val print = user + "@" + server + "/" + name + if_proper(ssh, " via ssh " + ssh.get) + val print = + "server " + user + "@" + server + "/" + name + if_proper(ssh, " via ssh " + ssh.get) val connection = DriverManager.getConnection(url, user, password) val db = new Database(connection, print, server, server_close)