src/Pure/Admin/build_log.scala
changeset 69299 2fd070377c99
parent 68169 395432e7516e
child 69980 f2e3adfd916f
--- 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))