src/Pure/System/system_channel.scala
changeset 79048 caddfe4949a8
parent 75393 87ebf5a50283
child 79049 10b6add456d0
--- a/src/Pure/System/system_channel.scala	Fri Nov 24 11:31:15 2023 +0100
+++ b/src/Pure/System/system_channel.scala	Fri Nov 24 14:11:01 2023 +0100
@@ -31,11 +31,12 @@
       val out_stream = socket.getOutputStream
       val in_stream = socket.getInputStream
 
-      if (Byte_Message.read_line(in_stream).map(_.text) == Some(password)) (out_stream, in_stream)
-      else {
-        out_stream.close()
-        in_stream.close()
-        error("Failed to connect system channel: bad password")
+      Byte_Message.read_line(in_stream) match {
+        case Some(bs) if bs.text == password => (out_stream, in_stream)
+        case _ =>
+          out_stream.close()
+          in_stream.close()
+          error("Failed to connect system channel: bad password")
       }
     }
     finally { shutdown() }