# HG changeset patch
# User wenzelm
# Date 1700941653 -3600
# Node ID 07799c394b6d37b9b24f7c9418bda0259e732b67
# Parent  a54be9630ef89fd0c7457885f4d254d229e5b10e
clarified signature;

diff -r a54be9630ef8 -r 07799c394b6d src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Nov 25 20:41:18 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Nov 25 20:47:33 2023 +0100
@@ -807,10 +807,10 @@
     def read_domain(
       db: SQL.Database,
       table: SQL.Table,
-      column: SQL.Column,
       restriction: Option[Iterable[String]] = None,
       cache: XML.Cache = XML.Cache.make()
     ): Set[String] = {
+      val column = Column.log_name
       db.execute_query_statement(
         table.select(List(column),
           sql = restriction match {
@@ -1113,9 +1113,7 @@
 
       abstract class Table_Status(table: SQL.Table) {
         private val known =
-          Synchronized(
-            private_data.read_domain(db, table, Column.log_name,
-              restriction = files_domain, cache = cache))
+          Synchronized(private_data.read_domain(db, table, restriction = files_domain, cache = cache))
 
         def required(file: JFile): Boolean = !(known.value)(Log_File.plain_name(file))
         def required(log_file: Log_File): Boolean = !(known.value)(log_file.name)