src/Pure/Tools/build_job.scala
changeset 72882 1dc2ad97e062
parent 72881 220a094a42d8
child 72958 0d8bc0252e2e
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 22:57:25 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 23:29:11 2020 +0100
@@ -460,7 +460,10 @@
           }
           else (Nil, Nil)
         }
-        catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }
+        catch {
+          case exn: Presentation.Build_Error => (exn.log_lines, List(exn.message))
+          case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
+        }
 
       val result =
       {