# HG changeset patch
# User wenzelm
# Date 1678820797 -3600
# Node ID c82d49a56cf976064efdf83205d35eb65ab03f98
# Parent  b45fc98d11ea8c184e377fc13d221c93d4c942fd
tuned signature: removed redundant argument;

diff -r b45fc98d11ea -r c82d49a56cf9 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 20:04:48 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 20:06:37 2023 +0100
@@ -334,23 +334,19 @@
       def sql(
         build_uuid: String = "",
         worker_uuid: String = "",
-        name: String = "",
         names: Iterable[String] = Nil
       ): SQL.Source =
         SQL.and(
           if_proper(build_uuid, Generic.build_uuid.equal(build_uuid)),
           if_proper(worker_uuid, Generic.worker_uuid.equal(worker_uuid)),
-          if_proper(name, Generic.name.equal(name)),
           if_proper(names, Generic.name.member(names)))
 
       def sql_where(
         build_uuid: String = "",
         worker_uuid: String = "",
-        name: String = "",
         names: Iterable[String] = Nil
       ): SQL.Source = {
-        SQL.where(sql(build_uuid = build_uuid, worker_uuid = worker_uuid,
-          name = name, names = names))
+        SQL.where(sql(build_uuid = build_uuid, worker_uuid = worker_uuid, names = names))
       }
     }