# HG changeset patch
# User wenzelm
# Date 1689337553 -7200
# Node ID ef1664be143d0744b2ad7d2edb88713b907a0d12
# Parent  5f14f1290a8874efad4ee88e00b887bfe734da8a
tuned;

diff -r 5f14f1290a88 -r ef1664be143d src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Jul 14 14:21:22 2023 +0200
+++ b/src/Pure/General/sql.scala	Fri Jul 14 14:25:53 2023 +0200
@@ -595,22 +595,19 @@
     if (user == "") error("Undefined database user")
 
     val db_host = proper_string(host) getOrElse "localhost"
-    val db_port = if (port > 0 && port != default_port) ":" + port else ""
-    val db_name = "/" + (proper_string(database) getOrElse user)
+    val db_port = if (port > 0) port else default_port
+    val db_name = proper_string(database) getOrElse user
 
     val fw =
       ssh match {
         case None =>
-          SSH.local_port_forwarding(port = if (port > 0) port else default_port, host = db_host)
+          SSH.local_port_forwarding(port = db_port, host = db_host)
         case Some(ssh) =>
-          ssh.port_forwarding(
-            remote_port = if (port > 0) port else default_port,
-            remote_host = db_host,
-            ssh_close = ssh_close)
+          ssh.port_forwarding(remote_port = db_port, remote_host = db_host, ssh_close = ssh_close)
       }
     try {
-      val url = "jdbc:postgresql://" + fw.host + ":" + fw.port + db_name
-      val name = user + "@" + fw + db_name + if_proper(ssh, " via ssh " + ssh.get)
+      val url = "jdbc:postgresql://" + fw.host + ":" + fw.port + "/" + db_name
+      val name = user + "@" + fw + "/" + db_name + if_proper(ssh, " via ssh " + ssh.get)
       val connection = DriverManager.getConnection(url, user, password)
       connection.setTransactionIsolation(transaction_isolation)
       new Database(name, connection, fw)