# HG changeset patch # User wenzelm # Date 1476115803 -7200 # Node ID e8407039b5725b98bc77686784c421c4fb122b9b # Parent c2594513687b2d8e58742d65aa79b2608cfc6bbe proper hierarchic names; diff -r c2594513687b -r e8407039b572 src/Pure/General/ssh.scala --- 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) }