src/Pure/Admin/build_history.scala
changeset 77799 3fb2c47a7605
parent 77792 b81b2c50fc7c
child 78162 41a87c4ea765
--- a/src/Pure/Admin/build_history.scala	Sun Apr 09 19:10:01 2023 +0200
+++ b/src/Pure/Admin/build_history.scala	Sun Apr 09 23:09:24 2023 +0200
@@ -345,7 +345,11 @@
               catch { case _: java.sql.SQLException => Nil }
             }
             else Nil
-          errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
+          for (msg <- errors)
+          yield {
+            val content = Library.encode_lines(Output.clean_yxml(msg))
+            List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> content)
+          }
         }
 
       build_out_progress.echo("Reading heap sizes ...")