--- a/src/Pure/Build/build.scala Fri Sep 06 15:46:51 2024 +0200
+++ b/src/Pure/Build/build.scala Fri Sep 06 15:59:48 2024 +0200
@@ -793,8 +793,8 @@
def check(filter: List[Regex], make_string: => String): Boolean =
filter.isEmpty || {
- val s = Output.clean_yxml(make_string)
- filter.forall(r => r.findFirstIn(Output.clean_yxml(s)).nonEmpty)
+ val s = Protocol_Message.clean_output(make_string)
+ filter.forall(r => r.findFirstIn(Protocol_Message.clean_output(s)).nonEmpty)
}
def print(session_name: String): Unit = {