# HG changeset patch
# User wenzelm
# Date 1692693075 -7200
# Node ID c06a0396b09dc3eaa31585b704653b960e1ac8f2
# Parent  39f6f180008d627e67eced4a80dc8fed07d6bc7b
tuned output;

diff -r 39f6f180008d -r c06a0396b09d src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Aug 22 10:05:03 2023 +0200
+++ b/src/Pure/General/sql.scala	Tue Aug 22 10:31:15 2023 +0200
@@ -676,7 +676,8 @@
     val url = "jdbc:postgresql://" + server.host + ":" + server.port + "/" + name
     val ssh = server.ssh_system.ssh_session
     val print =
-      "server " + user + "@" + server + "/" + name + if_proper(ssh, " via ssh " + ssh.get)
+      "server " + quote(user + "@" + server + "/" + name) +
+        if_proper(ssh, " via ssh " + quote(ssh.get.toString))
 
     val connection = DriverManager.getConnection(url, user, password)
     val db = new Database(connection, print, server, server_close)