changeset 65636 | df804cdba5f9 |
parent 65633 | 826311fca263 |
child 65639 | 4c14da234221 |
--- a/src/Pure/Admin/build_log.scala Sat Apr 29 19:43:04 2017 +0200 +++ b/src/Pure/Admin/build_log.scala Sat Apr 29 20:15:26 2017 +0200 @@ -645,7 +645,8 @@ user = user, password = password, database = database, host = host, port = port, ssh = if (ssh_host == "") None - else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port))) + else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)), + ssh_close = true) } def write_info(db: SQL.Database, files: List[JFile])