changeset 72213 | 6157757bb133 |
parent 72212 | 53e8858b839f |
child 72294 | 25c6423ec538 |
--- 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 {