# HG changeset patch
# User wenzelm
# Date 1708541657 -3600
# Node ID ade429ddb1fc7fc1d68a8f626e0569cceaff061e
# Parent  1fa1b32b037901bec1ca7fc3bb803e29395e4f33
more accurate types;

diff -r 1fa1b32b0379 -r ade429ddb1fc src/Pure/ML/ml_heap.scala
--- 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 " +