# HG changeset patch
# User wenzelm
# Date 1718531725 -7200
# Node ID 10f47bb1abd3b731a7732e5447abc0454a0e6e31
# Parent  605e1931934344369e1a1cd84c3a99495e55d236
tuned;

diff -r 605e19319343 -r 10f47bb1abd3 src/Pure/PIDE/byte_message.scala
--- a/src/Pure/PIDE/byte_message.scala	Sun Jun 16 11:50:42 2024 +0200
+++ b/src/Pure/PIDE/byte_message.scala	Sun Jun 16 11:55:25 2024 +0200
@@ -90,8 +90,9 @@
     }
 
   def write_line_message(stream: OutputStream, msg: Bytes): Unit = {
-    if (is_length(msg) || is_terminated(msg))
+    if (is_length(msg) || is_terminated(msg)) {
       error ("Bad content for line message:\n" ++ msg.text.take(100))
+    }
 
     val n = msg.size
     write(stream,