--- 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()
}
}