author | wenzelm |
Tue, 12 Dec 2017 17:47:23 +0100 | |
changeset 67190 | 58ab7ddbdb04 |
parent 67189 | 725897bbabef |
child 67191 | 9ab34bb83a84 |
--- a/src/Pure/Thy/latex.scala Tue Dec 12 17:47:00 2017 +0100 +++ b/src/Pure/Thy/latex.scala Tue Dec 12 17:47:23 2017 +0100 @@ -96,7 +96,7 @@ object File_Line_Error { - val Pattern = """^(.*):(\d+): (.*)$""".r + val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r def unapply(line: String): Option[(Path, Int, String)] = line match { case Pattern(file, Value.Int(line), message) =>