--- a/src/Pure/System/progress.scala Sat Mar 04 12:43:35 2023 +0100
+++ b/src/Pure/System/progress.scala Sat Mar 04 12:59:22 2023 +0100
@@ -88,13 +88,15 @@
extends Progress {
override def echo(message: Progress.Message): Unit =
Output.output(message.output_text, stdout = !stderr, include_empty = true)
+
+ override def toString: String = super.toString + ": console"
}
class File_Progress(path: Path, override val verbose: Boolean = false) extends Progress {
override def echo(message: Progress.Message): Unit =
File.append(path, message.output_text + "\n")
- override def toString: String = path.toString
+ override def toString: String = super.toString + ": " + path.toString
}