# HG changeset patch
# User wenzelm
# Date 1598524986 -7200
# Node ID 6157757bb13330e218dd31aee154003f5c261b07
# Parent  53e8858b839fea2d249c0b9981aae67172461537
tuned;

diff -r 53e8858b839f -r 6157757bb133 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Thu Aug 27 12:34:10 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Thu Aug 27 12:43:06 2020 +0200
@@ -85,9 +85,9 @@
     private var session: Session = null
     private var monitoring: Future[Unit] = Future.value(())
 
-    override def init(init_session: Session): Unit = synchronized
+    override def init(session: Session): Unit = synchronized
     {
-      session = init_session
+      this.session = session
     }
 
     override def exit(): Unit = synchronized
diff -r 53e8858b839f -r 6157757bb133 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Thu Aug 27 12:34:10 2020 +0200
+++ b/src/Pure/System/scala.scala	Thu Aug 27 12:43:06 2020 +0200
@@ -160,8 +160,8 @@
     private var session: Session = null
     private var futures = Map.empty[String, Future[Unit]]
 
-    override def init(init_session: Session): Unit =
-      synchronized { session = init_session }
+    override def init(session: Session): Unit =
+      synchronized { this.session = session }
 
     override def exit(): Unit = synchronized
     {