changeset 67187 | 3457d7d43ee9 |
parent 67180 | dcac4659d482 |
child 67201 | 4cffa4791ef7 |
--- a/src/Pure/Thy/present.scala Tue Dec 12 12:35:01 2017 +0100 +++ b/src/Pure/Thy/present.scala Tue Dec 12 13:34:11 2017 +0100 @@ -209,7 +209,7 @@ if (!result.ok) { cat_error(cat_lines(Latex.latex_errors(dir, root_name)), - "Failed to build document in directory " + File.path(dir.absolute_file)) + "Failed to build document in " + File.path(dir.absolute_file)) } bash("[ -f " + root_bash(document_format) + " ] && cp -f " +