--- a/src/Pure/Tools/build_job.scala Sun May 23 21:03:32 2021 +0200
+++ b/src/Pure/Tools/build_job.scala Sun May 23 22:46:30 2021 +0200
@@ -204,6 +204,7 @@
do_store: Boolean,
verbose: Boolean,
val numa_node: Option[Int],
+ log: Logger,
command_timings0: List[Properties.T])
{
val options: Options = NUMA.policy_options(info.options, numa_node)
@@ -232,7 +233,8 @@
}
else Nil
- val resources = new Resources(sessions_structure, base, command_timings = command_timings0)
+ val resources =
+ new Resources(sessions_structure, base, log = log, command_timings = command_timings0)
val session =
new Session(options, resources) {
override val cache: XML.Cache = store.cache
@@ -389,6 +391,8 @@
{
case msg: Prover.Output =>
val message = msg.message
+ if (msg.is_syslog) resources.log(msg.toString)
+
if (msg.is_stdout) {
stdout ++= Symbol.encode(XML.content(message))
}