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 = {