# HG changeset patch
# User wenzelm
# Date 1605819557 -3600
# Node ID 0d3224b3a92cd3a6f9eaeecbfa542443347430c1
# Parent  e9030100f97da0be461f8b23e8c059e3983aa3bc
proper message;

diff -r e9030100f97d -r 0d3224b3a92c src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu Nov 19 21:23:12 2020 +0100
+++ b/src/Pure/System/progress.scala	Thu Nov 19 21:59:17 2020 +0100
@@ -32,7 +32,7 @@
 
   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
   def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
-  def echo_document(msg: String) { echo(Output.error_message_text(msg)) }
+  def echo_document(msg: String) { echo(msg) }
 
   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
     Timing.timeit(message, enabled, echo)(e)