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