diff -r 8c5eedb6c983 -r c51e1cef1eae src/Pure/General/socket_io.ML --- a/src/Pure/General/socket_io.ML Tue Jun 21 16:03:00 2022 +0200 +++ b/src/Pure/General/socket_io.ML Tue Jun 21 22:17:11 2022 +0200 @@ -96,6 +96,6 @@ fun with_streams' f socket_name password = with_streams (fn streams => - (Byte_Message.write_line (#2 streams) password; f streams)) socket_name; + (Byte_Message.write_line (#2 streams) (Bytes.string password); f streams)) socket_name; end;