diff -r 2f4cb9cb087f -r ecb31c3bf980 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon May 17 15:01:37 2021 +0200 +++ b/src/Pure/Tools/build_job.scala Mon May 17 16:15:25 2021 +0200 @@ -447,7 +447,7 @@ using(store.open_database_context())(db_context => { val documents = - Presentation.build_documents(session_name, deps, db_context, + Document_Build.build_documents(session_name, deps, db_context, output_sources = info.document_output, output_pdf = info.document_output, progress = progress, @@ -460,7 +460,7 @@ else (Nil, Nil) } catch { - case exn: Presentation.Build_Error => (exn.log_lines, List(exn.message)) + case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message)) case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }