tuned;

--- a/src/Pure/Tools/server.scala	Fri Jul 05 12:53:45 2024 +0200
+++ b/src/Pure/Tools/server.scala	Fri Jul 05 13:04:39 2024 +0200
@@ -189,7 +189,7 @@
       catch { case _: IOException => }
 
     def write_line_message(msg: String): Unit =
-      out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
+      out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(msg)) }
 
     def write_byte_message(chunks: List[Bytes]): Unit =
       out_lock.synchronized { Byte_Message.write_message(out, chunks) }