changeset 77117 | 9a22256b0a27 |
parent 75968 | 5a782ca6872b |
child 77121 | ceee2a01322e |
--- a/src/Pure/Admin/build_status.scala Sat Jan 28 13:44:00 2023 +0100 +++ b/src/Pure/Admin/build_status.scala Sat Jan 28 15:04:15 2023 +0100 @@ -502,7 +502,7 @@ val image = Image(plot_name, image_width, image_height) val chart = session.ml_statistics.chart( - fields._1 + ": " + session.ml_statistics.heading, fields._2) + fields.title + ": " + session.ml_statistics.heading, fields.names) Graphics_File.write_chart_png( (dir + image.path).file, chart, image.width, image.height) image