src/Pure/ML/ml_statistics.scala
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