changeset 67417 | 34522db6b85a |
parent 67196 | eb29f4868d14 |
child 67418 | 5a6ed2e679fb |
--- a/src/Pure/Thy/latex.scala Sat Jan 13 12:19:03 2018 +0100 +++ b/src/Pure/Thy/latex.scala Sat Jan 13 12:51:03 2018 +0100 @@ -145,6 +145,10 @@ rest1 match { case More_Error(msg2) :: rest2 => filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) + case msg2 :: rest2 + if msg1.startsWith("Undefined control sequence") && + msg2.startsWith("\\") && msg2.containsSlice("->") => + filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) case _ => filter(rest1, (msg1, pos) :: result) }