# HG changeset patch
# User wenzelm
# Date 1700831461 -3600
# Node ID caddfe4949a8b389cad86dc49f6d8d8d2bfda253
# Parent  13afea5203f11d59a2cead80aa062c994d4eeb14
tuned;

diff -r 13afea5203f1 -r caddfe4949a8 src/Pure/System/system_channel.scala
--- 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() }