Skip to content

Commit

Permalink
Closes #81
Browse files Browse the repository at this point in the history
  • Loading branch information
sylvainhalle committed Aug 5, 2019
1 parent 74f22c1 commit d8b588b
Showing 1 changed file with 4 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -556,6 +556,10 @@ protected void fetchIncludes(/*@ non_null @*/ AnnotatedString as)
if (mat.find())
{
String filename = mat.group(2).trim();
if (!filename.endsWith(".tex"))
{
filename += ".tex";
}
m_innerFiles.add(filename);
}
}
Expand Down

0 comments on commit d8b588b

Please sign in to comment.