| changeset 73367 | 77ef8bef0593 | 
| parent 73359 | d8a0e996614b | 
| child 73522 | b219774a71ae | 
--- a/src/Pure/ML/ml_statistics.scala Thu Mar 04 19:55:52 2021 +0100 +++ b/src/Pure/ML/ml_statistics.scala Thu Mar 04 21:04:27 2021 +0100 @@ -93,7 +93,7 @@ override def exit(): Unit = synchronized { session = null - monitoring.cancel + monitoring.cancel() } private def consume(props: Properties.T): Unit = synchronized