# HG changeset patch
# User wenzelm
# Date 1658920652 -7200
# Node ID e174568d52d24ed5933715a8356ae871c4ffee90
# Parent  a068fb7346efaf452b3b00ced314dcca2f40d97a
tuned;

diff -r a068fb7346ef -r e174568d52d2 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Wed Jul 27 13:13:59 2022 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Jul 27 13:17:32 2022 +0200
@@ -84,7 +84,7 @@
           // prevent spurious garbage on the main protocol channel
           val orig_out = System.out
           try {
-            System.setOut(new PrintStream(new OutputStream { def write(n: Int): Unit = {} }))
+            System.setOut(new PrintStream(OutputStream.nullOutputStream()))
             server.start()
           }
           finally { System.setOut(orig_out) }