# HG changeset patch
# User wenzelm
# Date 1607637445 -3600
# Node ID 220a094a42d85bb11b72d4941a3dbdf1a6533f19
# Parent  2fce0ce47627ed286d76f8ad1e87bada5ecf93b9
proper else statement;

diff -r 2fce0ce47627 -r 220a094a42d8 src/Pure/Tools/build_job.scala
--- 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)) }