diff -r 34a746383c9b -r 4643bb10d188 src/Pure/System/progress.scala --- 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)