| changeset 64045 | c6160d0b0337 |
| parent 64041 | fd454d9e97c4 |
| child 65051 | f094e27e4902 |
--- a/src/Pure/Tools/ml_statistics.scala Tue Oct 04 20:20:21 2016 +0200 +++ b/src/Pure/Tools/ml_statistics.scala Tue Oct 04 21:11:35 2016 +0200 @@ -25,7 +25,7 @@ def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics = new ML_Statistics(session_name, ml_statistics) - def apply(info: Build.Session_Log_Info): ML_Statistics = + def apply(info: Build_Log.Session_Info): ML_Statistics = apply(info.session_name, info.ml_statistics) val empty = apply("", Nil)