tuned;
authorwenzelm
Thu May 18 14:41:40 2017 +0200 (2017-05-18)
changeset 6586865e132abab1e
parent 65867 53613acb76e7
child 65870 81574a7e7c38
tuned;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Thu May 18 14:41:20 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Thu May 18 14:41:40 2017 +0200
     1.3 @@ -330,8 +330,8 @@
     1.4                    """ using 1:6 smooth csplines title "maximum heap" """,
     1.5                    """ using 1:7 smooth sbezier title "average heap (smooth)" """,
     1.6                    """ using 1:7 smooth csplines title "average heap" """,
     1.7 -                  """ using 1:8 smooth sbezier title "final heap (smooth)" """,
     1.8 -                  """ using 1:8 smooth csplines title "final heap" """)
     1.9 +                  """ using 1:8 smooth sbezier title "stored heap (smooth)" """,
    1.10 +                  """ using 1:8 smooth csplines title "stored heap" """)
    1.11  
    1.12                def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image =
    1.13                {