| changeset 83282 | 4643bb10d188 |
| parent 83280 | a3c59c842625 |
| child 83283 | 93a0271aa837 |
--- a/src/Pure/System/progress.scala Wed Oct 15 11:14:15 2025 +0200 +++ b/src/Pure/System/progress.scala Wed Oct 15 11:17:49 2025 +0200 @@ -224,7 +224,7 @@ } class File_Progress(path: Path, override val verbose: Boolean = false) -extends Progress { +extends Progress with Progress.Status { override def output(msgs: Progress.Output): Unit = synchronized { val txt = output_text(msgs, terminate = true) if (txt.nonEmpty) File.append(path, txt)