src/Pure/System/progress.scala
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)