--- a/src/Pure/Tools/build_job.scala Thu Dec 10 22:46:12 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Dec 10 22:57:25 2020 +0100
@@ -444,8 +444,7 @@
val (document_output, 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) {
using(store.open_database_context())(db_context =>
{
val documents =
@@ -459,7 +458,7 @@
(documents.flatMap(_.log_lines), Nil)
})
}
- (Nil, Nil)
+ else (Nil, Nil)
}
catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }