# HG changeset patch
# User wenzelm
# Date 1542192663 -3600
# Node ID 2fd070377c997408434d8debb22476a087dc3617
# Parent  085f31ae902d8b52f80efdc0db8d70c8feed21df
clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");

diff -r 085f31ae902d -r 2fd070377c99 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Nov 13 20:57:54 2018 +0100
+++ b/src/Pure/Admin/build_log.scala	Wed Nov 14 11:51:03 2018 +0100
@@ -146,9 +146,6 @@
       name != "main.log"
     }
 
-    def find_files(dirs: Iterable[Path]): List[JFile] =
-      dirs.iterator.flatMap(dir => File.find_files(dir.file, is_log(_))).toList
-
 
     /* date format */
 
@@ -904,7 +901,10 @@
 
     def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
     {
-      write_info(db, Log_File.find_files(dirs), ml_statistics = ml_statistics)
+      val log_files =
+        dirs.flatMap(dir =>
+          File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true))
+      write_info(db, log_files, ml_statistics = ml_statistics)
 
       db.create_view(Data.pull_date_table())
       db.create_view(Data.pull_date_table(afp = true))
diff -r 085f31ae902d -r 2fd070377c99 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Nov 13 20:57:54 2018 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 14 11:51:03 2018 +0100
@@ -151,7 +151,7 @@
     start: JFile,
     pred: JFile => Boolean = _ => true,
     include_dirs: Boolean = false,
-    follow_links: Boolean = true): List[JFile] =
+    follow_links: Boolean = false): List[JFile] =
   {
     val result = new mutable.ListBuffer[JFile]
     def check(file: JFile) { if (pred(file)) result += file }