# HG changeset patch
# User wenzelm
# Date 1611085085 -3600
# Node ID e2132e1553a94faddf5a726174d4e1dd045de473
# Parent  624c2b98860af47d0e18f65eb47d97833eea5543
proper heap_free;

diff -r 624c2b98860a -r e2132e1553a9 src/Pure/System/java_statistics.scala
--- a/src/Pure/System/java_statistics.scala	Tue Jan 19 20:23:13 2021 +0100
+++ b/src/Pure/System/java_statistics.scala	Tue Jan 19 20:38:05 2021 +0100
@@ -21,8 +21,8 @@
   def memory_status(): Memory_Status =
   {
     val heap_size = Runtime.getRuntime.totalMemory()
-    val heap_used = heap_size - Runtime.getRuntime.freeMemory()
-    Memory_Status(heap_size, heap_used)
+    val heap_free = Runtime.getRuntime.freeMemory()
+    Memory_Status(heap_size, heap_free)
   }