# HG changeset patch
# User wenzelm
# Date 1525896249 -7200
# Node ID 2a5ae592eafb41d2f024fbbf00d4e214a474bfb3
# Parent  62a3294edda36d8c41047c3e1916cbc3f61fb162
more informative error, notably for missing executable;

diff -r 62a3294edda3 -r 2a5ae592eafb src/Pure/Thy/present.scala
--- 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))
     }