clarified file pattern;
authorwenzelm
Tue, 12 Dec 2017 17:47:23 +0100
changeset 67190 58ab7ddbdb04
parent 67189 725897bbabef
child 67191 9ab34bb83a84
clarified file pattern;
src/Pure/Thy/latex.scala
--- 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) =>