| changeset 73164 | e2132e1553a9 |
| parent 72250 | 13976f92a2d0 |
| child 75393 | 87ebf5a50283 |
--- 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) }