author | wenzelm |
Mon, 16 Jan 2023 22:41:00 +0100 | |
changeset 76997 | d481dc154310 |
parent 76996 | 6d847e27cafc |
child 76998 | 9096703ed99e |
child 77001 | 68f1fc53c8fd |
--- a/src/Pure/System/progress.scala Mon Jan 16 20:57:38 2023 +0100 +++ b/src/Pure/System/progress.scala Mon Jan 16 22:41:00 2023 +0100 @@ -122,7 +122,7 @@ (results, message) } - (results, List(XML.Elem(Markup(Markup.TRACING_MESSAGE, Nil), message))) + (results, List(XML.elem(Markup.TRACING_MESSAGE, message))) } } }