# HG changeset patch
# User wenzelm
# Date 1674842388 -3600
# Node ID 97a425ecf96de76d49039ef8194d0abbdd532d77
# Parent  6608de52a3b585d4e4c17595b75feefa6b1ad2b7
tuned;

diff -r 6608de52a3b5 -r 97a425ecf96d src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Fri Jan 27 17:33:49 2023 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Jan 27 18:59:48 2023 +0100
@@ -116,8 +116,9 @@
   def mem_scale(x: Long): Long = x / 1024 / 1024
 
   def mem_field_scale(name: String, x: Double): Double =
-    if (heap_fields._2.contains(name) || program_fields._2.contains(name))
+    if (heap_fields._2.contains(name) || program_fields._2.contains(name)) {
       mem_scale(x.toLong).toDouble
+    }
     else x
 
   val CODE_SIZE = "size_code"