changeset 72596 | b2bbe2e6575d |
parent 72574 | d892f6d66402 |
child 72613 | d01ea9e3bd2d |
--- a/src/Pure/Tools/build.scala Thu Nov 12 11:46:53 2020 +0100 +++ b/src/Pure/Tools/build.scala Thu Nov 12 12:10:17 2020 +0100 @@ -386,7 +386,7 @@ Present.finish(store.browser_info, graph_pdf, info, session_name) Nil } - catch { case ERROR(msg) => List(msg) case e@Exn.Interrupt() => List(Exn.message(e)) } + catch { case Exn.Interrupt.ERROR(msg) => List(msg) } val result = {