# HG changeset patch
# User wenzelm
# Date 1698577021 -3600
# Node ID 763dd9bdb101b0722817b2300a870f230f13b6cb
# Parent  a79bd9d82c000748fe9fa1d5c5b5f5c23f9358aa
clarified message;

diff -r a79bd9d82c00 -r 763dd9bdb101 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Oct 29 11:49:33 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Oct 29 11:57:01 2023 +0100
@@ -1209,7 +1209,7 @@
       var ml_statistics: Boolean = false
       var snapshot: Option[Path] = None
       var vacuum = false
-      var dirs: List[Path] = Nil
+      var logs: List[Path] = Nil
       var options = Options.init()
       var verbose = false
 
@@ -1220,17 +1220,17 @@
     -M           include ML statistics
     -S FILE      snapshot to SQLite db file
     -V           vacuum cleaning of database
-    -d DIR       include directory with log files
+    -d LOG       include log file start location
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
 
-  Update the build_log database server from log files, recursively collected
-  from given directories.
+  Update the build_log database server from log files, which are recursively
+  collected from given start locations (files or directories).
 """,
         "M" -> (_ => ml_statistics = true),
         "S:" -> (arg => snapshot = Some(Path.explode(arg))),
         "V" -> (_ => vacuum = true),
-        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+        "d:" -> (arg => logs = logs ::: List(Path.explode(arg))),
         "o:" -> (arg => options = options + arg),
         "v" -> (_ => verbose = true))
 
@@ -1239,7 +1239,7 @@
 
       val progress = new Console_Progress(verbose = verbose)
 
-      build_log_database(options, dirs, progress = progress, vacuum = vacuum,
+      build_log_database(options, logs, progress = progress, vacuum = vacuum,
         ml_statistics = ml_statistics, snapshot = snapshot)
     })
 }