--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Apr 27 11:41:13 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Apr 27 15:56:55 2017 +0200
@@ -89,7 +89,7 @@
sealed case class Remote_Build(
host: String,
user: String = "",
- port: Int = SSH.default_port,
+ port: Int = 0,
shared_home: Boolean = true,
options: String = "",
args: String = "")
--- a/src/Pure/Admin/remote_dmg.scala Thu Apr 27 11:41:13 2017 +0200
+++ b/src/Pure/Admin/remote_dmg.scala Thu Apr 27 15:56:55 2017 +0200
@@ -32,14 +32,14 @@
Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
{
Command_Line.tool0 {
- var port = SSH.default_port
+ var port = 0
var volume_name = ""
val getopts = Getopts("""
Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
Options are:
- -p PORT alternative SSH port (default: """ + SSH.default_port + """)
+ -p PORT alternative SSH port
-V NAME specify volume name
Turn the contents of a tar.gz file into a dmg file -- produced on a remote
--- 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))
--- a/src/Pure/General/ssh.scala Thu Apr 27 11:41:13 2017 +0200
+++ b/src/Pure/General/ssh.scala Thu Apr 27 15:56:55 2017 +0200
@@ -74,9 +74,10 @@
{
def update_options(new_options: Options): Context = new Context(new_options, jsch)
- def open_session(host: String, user: String = "", port: Int = default_port): Session =
+ def open_session(host: String, user: String = "", port: Int = 0): Session =
{
- val session = jsch.getSession(if (user == "") null else user, host, port)
+ val session =
+ jsch.getSession(if (user == "") null else user, host, if (port > 0) port else default_port)
session.setUserInfo(No_User_Info)
session.setServerAliveInterval(alive_interval(options))