src/Pure/General/file.scala
changeset 69301 f6c17b9e1104
parent 69300 8b6ab9989bcd
child 69393 ed0824ef337e
--- a/src/Pure/General/file.scala	Wed Nov 14 16:26:58 2018 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 14 20:04:39 2018 +0100
@@ -170,7 +170,8 @@
           }
           override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
-            check(path.toFile)
+            val file = path.toFile
+            if (include_dirs || !file.isDirectory) check(file)
             FileVisitResult.CONTINUE
           }
         }