# HG changeset patch
# User wenzelm
# Date 1677931162 -3600
# Node ID daf632e9ce7e56a5a5272e890940ba38fed41e1d
# Parent  2e2b2bd6b2d2382832d9f892a9dfd60ffc57d5b1
tuned messages;

diff -r 2e2b2bd6b2d2 -r daf632e9ce7e src/Pure/System/progress.scala
--- 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
 }