src/Pure/Admin/build_log.scala
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])