tuned;
authorwenzelm
Sat, 01 Nov 2025 14:22:26 +0100
changeset 83438 cd9ecdf1c64c
parent 83437 0556adb3581b
child 83439 de01fc022709
tuned;
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()
     }
   }