# HG changeset patch
# User wenzelm
# Date 1762003346 -3600
# Node ID cd9ecdf1c64cbe99cbb2f501cd1945af8d1067d9
# Parent  0556adb3581b000063420cd70a370c622b0db5af
tuned;

diff -r 0556adb3581b -r cd9ecdf1c64c src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Sat Nov 01 14:19:16 2025 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Sat Nov 01 14:22:26 2025 +0100
@@ -33,7 +33,7 @@
   private def read_header(): List[String] = {
     val header = new mutable.ListBuffer[String]
     var line = ""
-    while ({ line = read_line(); line != "" }) header += line
+    while ({ line = read_line(); line.nonEmpty }) header += line
     header.toList
   }
 
@@ -72,7 +72,7 @@
     out.synchronized {
       out.write(header)
       out.write(content)
-      out.flush
+      out.flush()
     }
   }