src/Pure/General/ssh.scala
changeset 66923 914935f8a462
parent 66570 9af879e222cc
child 67066 1645cef7a49c
--- 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))