tuned, following hints by IntelliJ IDEA;
authorwenzelm
Mon, 17 Oct 2022 14:24:35 +0200
changeset 76324 6108b1751c1b
parent 76323 3637a0d06fe1
child 76325 14cf5a50c1e9
tuned, following hints by IntelliJ IDEA;
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] =