# HG changeset patch
# User wenzelm
# Date 1542109066 -3600
# Node ID 72a9860f86020c6396db3e15ca6fc34d61be5bef
# Parent  06fda16e50fbb65b8670199f563ea6ff5cc3359e
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";

diff -r 06fda16e50fb -r 72a9860f8602 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Nov 13 11:30:44 2018 +0100
+++ b/src/Pure/General/file.scala	Tue Nov 13 12:37:46 2018 +0100
@@ -11,11 +11,12 @@
   OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
   InputStreamReader, File => JFile, IOException}
 import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
-  Files, SimpleFileVisitor, FileVisitResult}
+  Files, SimpleFileVisitor, FileVisitOption, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.regex.Pattern
+import java.util.EnumSet
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
@@ -149,14 +150,18 @@
   def find_files(
     start: JFile,
     pred: JFile => Boolean = _ => true,
-    include_dirs: Boolean = false): List[JFile] =
+    include_dirs: Boolean = false,
+    follow_links: Boolean = true): List[JFile] =
   {
     val result = new mutable.ListBuffer[JFile]
     def check(file: JFile) { if (pred(file)) result += file }
 
     if (start.isFile) check(start)
     else if (start.isDirectory) {
-      Files.walkFileTree(start.toPath,
+      val options =
+        if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS)
+        else EnumSet.noneOf(classOf[FileVisitOption])
+      Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE,
         new SimpleFileVisitor[JPath] {
           override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {