--- a/src/Pure/General/sqlite.scala Tue Oct 11 10:21:32 2016 +0200
+++ b/src/Pure/General/sqlite.scala Tue Oct 11 10:43:27 2016 +0200
@@ -27,7 +27,7 @@
{
override def toString: String = path.toString
- def close { connection.close }
+ def close() { connection.close }
def rebuild { using(statement("VACUUM"))(_.execute()) }
--- a/src/Pure/General/ssh.scala Tue Oct 11 10:21:32 2016 +0200
+++ b/src/Pure/General/ssh.scala Tue Oct 11 10:43:27 2016 +0200
@@ -36,6 +36,8 @@
}
}
+ val default_port = 22
+
/* init */
@@ -108,7 +110,7 @@
{
override def toString: String = kind + " " + session.toString
- def close { channel.disconnect }
+ def close() { channel.disconnect }
}
@@ -271,10 +273,10 @@
override def toString: String =
(if (session.getUserName == null) "" else session.getUserName + "@") +
(if (session.getHost == null) "" else session.getHost) +
- (if (session.getPort == 22) "" else ":" + session.getPort) +
+ (if (session.getPort == default_port) "" else ":" + session.getPort) +
(if (session.isConnected) "" else " (disconnected)")
- def close { session.disconnect }
+ def close() { session.disconnect }
def execute(command: String,
options: Options = session_options,
@@ -317,7 +319,7 @@
class SSH private(val options: Options, val jsch: JSch)
{
- def open_session(host: String, port: Int = 22, user: String = ""): SSH.Session =
+ def open_session(host: String, port: Int = SSH.default_port, user: String = ""): SSH.Session =
{
val session = jsch.getSession(if (user == "") null else user, host, port)