clarified file pattern;
authorwenzelm
Tue Dec 12 17:47:23 2017 +0100 (17 months ago)
changeset 6719058ab7ddbdb04
parent 67189 725897bbabef
child 67191 9ab34bb83a84
clarified file pattern;
src/Pure/Thy/latex.scala
     1.1 --- a/src/Pure/Thy/latex.scala	Tue Dec 12 17:47:00 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.scala	Tue Dec 12 17:47:23 2017 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4  
     1.5      object File_Line_Error
     1.6      {
     1.7 -      val Pattern = """^(.*):(\d+): (.*)$""".r
     1.8 +      val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
     1.9        def unapply(line: String): Option[(Path, Int, String)] =
    1.10          line match {
    1.11            case Pattern(file, Value.Int(line), message) =>