# HG changeset patch
# User wenzelm
# Date 1768688093 -3600
#      Sat Jan 17 23:14:53 2026 +0100
# Node ID 47a0e444953d84ede2a918fe52356b9eee89015e
# Parent  3ed2781b1cc5844cc87a642a872cb82f1c6c2aa0
test

diff -r 3ed2781b1cc5 -r 47a0e444953d src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Wed Jan 14 13:09:47 2026 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Jan 17 23:14:53 2026 +0100
@@ -1337,6 +1337,8 @@
     }
   }
 
+  val t0 = Time.now()
+
   def run(): Build.Results = {
     val vacuous =
       synchronized_database("Build_Process.init") {
@@ -1362,7 +1364,11 @@
               build_send(Build_Process.private_data.channel_ready)
             }
           }
-          while(!build_action()) {}
+          while(!build_action()) { }
+          val t = Time.now() - t0
+          val mem = Java_Statistics.memory_status()
+          File.append(Path.explode("a.dat"),
+            t.toString + " " + mem.heap_size.MiB + " " + mem.heap_used.MiB + "\n")
         }
       }
       finally {