changeset 77174 | 1eb55d6809b3 |
parent 77173 | f1063cdb0093 |
child 77184 | 861777e58b77 |
--- a/src/Tools/jEdit/src/document_dockable.scala Wed Feb 01 20:57:15 2023 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Wed Feb 01 21:23:54 2023 +0100 @@ -105,7 +105,7 @@ /* progress */ - class Log_Progress extends Program_Progress(default_program = "build") { + class Log_Progress extends Program_Progress(default_title = "build") { progress => override def detect_program(s: String): Option[String] =