# HG changeset patch
# User wenzelm
# Date 1638019871 -3600
# Node ID 01414167077442619c2dd281ee178b91fe549822
# Parent  7420a7ac1a4cfb857bcccbbaab531681a9d230bb
proper fields for gnuplot (amending b614e3e4146a);

diff -r 7420a7ac1a4c -r 014141670774 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Nov 27 14:03:44 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Nov 27 14:31:11 2021 +0100
@@ -423,10 +423,10 @@
                       entry.ml_timing.elapsed.minutes.toString,
                       entry.ml_timing.resources.minutes.toString,
                       entry.maximum_code.toString,
-                      entry.maximum_code.toString,
+                      entry.average_code.toString,
+                      entry.maximum_stack.toString,
                       entry.average_stack.toString,
-                      entry.maximum_stack.toString,
-                      entry.average_heap.toString,
+                      entry.maximum_heap.toString,
                       entry.average_heap.toString,
                       entry.stored_heap.toString).mkString(" "))))