--- 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,
--- 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 =