# HG changeset patch
# User wenzelm
# Date 1710186274 -3600
# Node ID 47705d905420edb1ccd7a9666033f876b0c81c0e
# Parent  c49cb2a1ec44369a61fc1509ded781ee33f1b464
tuned signature;

diff -r c49cb2a1ec44 -r 47705d905420 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Mon Mar 11 20:33:49 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Mon Mar 11 20:44:34 2024 +0100
@@ -336,10 +336,10 @@
       val name = SQL.Column.string("name")
 
       def build_id_table(table: SQL.Table): Boolean =
-        table.columns.exists(column => column.name == build_id.name)
+        table.columns.exists(_.equals_name(build_id))
 
       def build_uuid_table(table: SQL.Table): Boolean =
-        table.columns.exists(column => column.name == build_uuid.name)
+        table.columns.exists(_.equals_name(build_uuid))
 
       def sql(
         build_id: Long = 0,
diff -r c49cb2a1ec44 -r 47705d905420 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 11 20:33:49 2024 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 11 20:44:34 2024 +0100
@@ -142,6 +142,8 @@
     primary_key: Boolean = false,
     expr: SQL.Source = ""
   ) {
+    def equals_name(other: Column): Boolean = name == other.name
+
     def make_primary_key: Column = copy(primary_key = true)
 
     def apply(table: Table): Column =