# HG changeset patch
# User wenzelm
# Date 1698576573 -3600
# Node ID a79bd9d82c000748fe9fa1d5c5b5f5c23f9358aa
# Parent  66634877e34cbb0dbf3f9878d6db30b9fba43b42
tuned signature;

diff -r 66634877e34c -r a79bd9d82c00 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Oct 29 11:39:17 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Oct 29 11:49:33 2023 +0100
@@ -141,6 +141,10 @@
       name != "main.log"
     }
 
+    def find_files(starts: List[JFile]): List[JFile] =
+      starts.flatMap(start => File.find_files(start, pred = is_log(_), follow_links = true))
+        .sortBy(plain_name)
+
 
     /* date format */
 
@@ -1156,7 +1160,7 @@
 
   /** maintain build_log database **/
 
-  def build_log_database(options: Options, log_dirs: List[Path],
+  def build_log_database(options: Options, logs: List[Path],
     progress: Progress = new Progress,
     vacuum: Boolean = false,
     ml_statistics: Boolean = false,
@@ -1164,10 +1168,7 @@
   ): Unit = {
     val store = Build_Log.store(options)
 
-    val log_files =
-      log_dirs.flatMap(dir =>
-        File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true)
-      ).sortBy(Log_File.plain_name)
+    val log_files = Log_File.find_files(logs.map(_.file))
 
     using(store.open_database()) { db =>
       if (vacuum) db.vacuum()