author | wenzelm |
Mon, 10 Oct 2016 18:10:03 +0200 | |
changeset 64133 | e8407039b572 |
parent 64132 | c2594513687b |
child 64134 | 57581e4026fe |
--- a/src/Pure/General/ssh.scala Mon Oct 10 16:04:57 2016 +0200 +++ b/src/Pure/General/ssh.scala Mon Oct 10 18:10:03 2016 +0200 @@ -146,7 +146,9 @@ read_dir(dir).flatMap(entry => { val file = dir + "/" + entry.name - if (entry.is_dir) find(file) else if (pred(entry)) List(entry) else Nil + if (entry.is_dir) find(file) + else if (pred(entry)) List(entry.copy(name = file)) + else Nil }) find(remote_path) }