equal
deleted
inserted
replaced
678 val log_lines = result.out_lines ::: result.err_lines |
678 val log_lines = result.out_lines ::: result.err_lines |
679 |
679 |
680 if (!result.ok) { |
680 if (!result.ok) { |
681 val message = |
681 val message = |
682 Exn.cat_message( |
682 Exn.cat_message( |
683 Library.trim_line(result.err), |
683 result.err, |
684 cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)), |
684 cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)), |
685 "Failed to build document " + quote(doc.name)) |
685 "Failed to build document " + quote(doc.name)) |
686 throw new Build_Error(log_lines, message) |
686 throw new Build_Error(log_lines, message) |
687 } |
687 } |
688 else if (!result_path.is_file) { |
688 else if (!result_path.is_file) { |