src/Pure/Tools/build_job.scala
changeset 73777 52e43a93d51f
parent 73774 734d5d3fbd9d
child 73781 0909fd14f8a4
--- a/src/Pure/Tools/build_job.scala	Sun May 23 23:15:04 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Mon May 24 11:58:06 2021 +0200
@@ -203,8 +203,8 @@
   store: Sessions.Store,
   do_store: Boolean,
   verbose: Boolean,
+  log: Logger,
   val numa_node: Option[Int],
-  log: Logger,
   command_timings0: List[Properties.T])
 {
   val options: Options = NUMA.policy_options(info.options, numa_node)
@@ -391,7 +391,7 @@
         {
           case msg: Prover.Output =>
             val message = msg.message
-            if (msg.is_syslog) resources.log(msg.toString)
+            if (msg.is_system) resources.log(Protocol.message_text(message))
 
             if (msg.is_stdout) {
               stdout ++= Symbol.encode(XML.content(message))