author | wenzelm |
Wed, 21 Feb 2024 19:54:17 +0100 | |
changeset 79683 | ade429ddb1fc |
parent 79682 | 1fa1b32b0379 |
child 79684 | 0554a32a6ef4 |
--- a/src/Pure/ML/ml_heap.scala Wed Feb 21 19:36:53 2024 +0100 +++ b/src/Pure/ML/ml_heap.scala Wed Feb 21 19:54:17 2024 +0100 @@ -72,8 +72,8 @@ object Slices_Size { val name = Generic.name - val slice = SQL.Column.int("slice").make_primary_key - val size = SQL.Column.long("size") + val slice = Slices.slice + val size = SQL.Column.string("size") val table = make_table(List(name, slice, size), body = "SELECT name, slice, pg_size_pretty(length(content)::bigint) as size FROM " +