src/Tools/VSCode/src/channel.scala
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)