changeset 79861 | 47705d905420 |
parent 79860 | c49cb2a1ec44 |
child 79882 | 6f9ae0f052bc |
--- 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 =