author | wenzelm |
Wed, 09 May 2018 22:04:09 +0200 | |
changeset 68132 | 2a5ae592eafb |
parent 68131 | 62a3294edda3 |
child 68133 | f6a22490cca8 |
--- a/src/Pure/Thy/present.scala Wed May 09 22:03:02 2018 +0200 +++ b/src/Pure/Thy/present.scala Wed May 09 22:04:09 2018 +0200 @@ -272,6 +272,7 @@ if (!result.ok) { cat_error( + Library.trim_line(result.err), cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)), "Failed to build document in " + File.path(dir.absolute_file)) }