# HG changeset patch
# User wenzelm
# Date 1476542118 -7200
# Node ID 65f7d2eea2d7dc0e3627c655c51ab9df122074c9
# Parent  d78d46c755f811d3a88437abec0c14a2c88275bc
tuned signature;

diff -r d78d46c755f8 -r 65f7d2eea2d7 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Oct 15 15:42:11 2016 +0200
+++ b/src/Pure/General/ssh.scala	Sat Oct 15 16:35:18 2016 +0200
@@ -324,7 +324,7 @@
 {
   def update_options(new_options: Options): SSH = new SSH(new_options, jsch)
 
-  def open_session(host: String, port: Int = SSH.default_port, user: String = ""): SSH.Session =
+  def open_session(host: String, user: String = "", port: Int = SSH.default_port): SSH.Session =
   {
     val session = jsch.getSession(if (user == "") null else user, host, port)