author | wenzelm |
Mon, 17 Oct 2022 14:24:35 +0200 | |
changeset 76324 | 6108b1751c1b |
parent 76323 | 3637a0d06fe1 |
child 76325 | 14cf5a50c1e9 |
--- 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] =