# HG changeset patch
# User wenzelm
# Date 1720177479 -7200
# Node ID bbeb2f2049aa46663ac9b8d966cc6ad9b1505de4
# Parent  2a9abd6a164e7cad745f8acc31cdb120318cb76a
tuned;

diff -r 2a9abd6a164e -r bbeb2f2049aa src/Pure/Tools/server.scala
--- 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) }