--- a/src/Pure/General/ssh.scala Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/General/ssh.scala Fri Oct 27 11:46:03 2017 +0200
@@ -63,7 +63,7 @@
jsch.setKnownHosts(File.platform_path(known_hosts))
val identity_files =
- Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
+ space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
for (identity_file <- identity_files if identity_file.is_file)
jsch.addIdentity(File.platform_path(identity_file))