changeset 67856 | ec9f1ec763a0 |
parent 67805 | 2d9a265b294e |
child 68410 | 4e27f5c361d2 |
--- a/src/Tools/VSCode/src/channel.scala Wed Mar 14 15:08:46 2018 +0100 +++ b/src/Tools/VSCode/src/channel.scala Wed Mar 14 16:48:05 2018 +0100 @@ -98,7 +98,7 @@ /* progress */ - def make_progress(verbose: Boolean = false): Progress = + def progress(verbose: Boolean = false): Progress = new Progress { override def echo(msg: String): Unit = log_writeln(msg) override def echo_warning(msg: String): Unit = log_warning(msg)