--- a/src/Pure/Tools/build_job.scala Sat Nov 21 16:22:35 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Nov 21 17:12:17 2020 +0100
@@ -217,7 +217,8 @@
val document_errors =
try {
- if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
+ if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
+ {
val document_progress =
new Progress {
override def echo(msg: String): Unit =
@@ -226,8 +227,12 @@
progress.echo_document(msg)
}
val documents =
- Presentation.build_documents(session_name, deps, store, verbose = verbose,
- verbose_latex = true, progress = document_progress)
+ Presentation.build_documents(session_name, deps, store,
+ output_sources = info.document_output,
+ output_pdf = info.document_output,
+ progress = document_progress,
+ verbose = verbose,
+ verbose_latex = true)
using(store.open_database(session_name, output = true))(db =>
for ((doc, pdf) <- documents) {
db.transaction {