src/Pure/Tools/build.scala
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 =
         {