# HG changeset patch
# User wenzelm
# Date 1542225593 -3600
# Node ID 51d8b4dbc61b99457c89c8d7684d6f2057614bff
# Parent  5faf57207a9bbf71b0365619bd87c633bf25662d
more uniform wrt. File.find_files;

diff -r 5faf57207a9b -r 51d8b4dbc61b src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Nov 14 20:51:14 2018 +0100
+++ b/src/Pure/General/ssh.scala	Wed Nov 14 20:59:53 2018 +0100
@@ -395,8 +395,8 @@
 
       def find(dir: Path)
       {
+        if (include_dirs) check(dir)
         if (follow_links || !is_link(dir)) {
-          if (include_dirs) check(dir)
           for (entry <- read_dir(dir)) {
             val path = dir + Path.basic(entry.name)
             if (entry.is_file) check(path) else find(path)