| changeset 72212 | 53e8858b839f |
| parent 72157 | d1ca82e27cbc |
| child 72213 | 6157757bb133 |
--- a/src/Pure/ML/ml_statistics.scala Wed Aug 26 15:59:21 2020 +0100 +++ b/src/Pure/ML/ml_statistics.scala Thu Aug 27 12:34:10 2020 +0200 @@ -117,7 +117,7 @@ } } - val functions = List(Markup.ML_Statistics.name -> ml_statistics) + override val functions = List(Markup.ML_Statistics.name -> ml_statistics) }