# 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)
     }