diff -r 607f7ad07a60 -r 659305708959 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Thu Apr 27 11:41:13 2017 +0200 +++ b/src/Pure/General/sql.scala Thu Apr 27 15:56:55 2017 +0200 @@ -325,7 +325,7 @@ password: String, database: String = "", host: String = "", - port: Int = default_port, + port: Int = 0, ssh: Option[SSH.Session] = None): Database = { init_jdbc @@ -333,7 +333,7 @@ require(user != "") val db_host = if (host != "") host else "localhost" - val db_port = if (port != default_port) ":" + port else "" + val db_port = if (port > 0 && port != default_port) ":" + port else "" val db_name = "/" + (if (database != "") database else user) val (url, name, port_forwarding) = @@ -344,7 +344,9 @@ val name = user + "@" + spec (url, name, None) case Some(ssh) => - val fw = ssh.port_forwarding(remote_host = db_host, remote_port = port) + val fw = + ssh.port_forwarding(remote_host = db_host, + remote_port = if (port > 0) port else default_port) val url = "jdbc:postgresql://localhost:" + fw.local_port + db_name val name = user + "@" + fw + db_name + " via ssh " + ssh (url, name, Some(fw))