diff -r 3637a0d06fe1 -r 6108b1751c1b src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Mon Oct 17 14:11:59 2022 +0200 +++ b/src/Pure/Tools/server.scala Mon Oct 17 14:24:35 2022 +0200 @@ -173,7 +173,7 @@ writer_lock = out_lock) def read_password(password: String): Boolean = - try { Byte_Message.read_line(in).map(_.text) == Some(password) } + try { Byte_Message.read_line(in).map(_.text).contains(password) } catch { case _: IOException => false } def read_line_message(): Option[String] =