src/Pure/Thy/present.scala
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 " +