# HG changeset patch
# User wenzelm
# Date 1677962476 -3600
# Node ID 7d13996ffeccbf4eb8bca53332355192f0bf4a4b
# Parent  8dfe2fbc98e73eb20ea26bc8fbd3e7200616c0e7
proper "val verbose" (amending 2e2b2bd6b2d2);

diff -r 8dfe2fbc98e7 -r 7d13996ffecc src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Sat Mar 04 21:25:12 2023 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Sat Mar 04 21:41:16 2023 +0100
@@ -100,6 +100,7 @@
   def progress(verbose: Boolean = false): Progress = {
     val verbose_ = verbose
     new Progress {
+      override val verbose: Boolean = verbose_
       override def echo(message: Progress.Message): Unit =
         message.kind match {
           case Progress.Kind.writeln => log_writeln(message.text)