# HG changeset patch
# User wenzelm
# Date 1605179417 -3600
# Node ID b2bbe2e6575d4b305a77ee3e8ea4a56e85e99285
# Parent  c806eeb9138ccabedb5e15a77e019e1b7631d9c2
tuned signature;

diff -r c806eeb9138c -r b2bbe2e6575d src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Thu Nov 12 11:46:53 2020 +0100
+++ b/src/Pure/General/exn.scala	Thu Nov 12 12:10:17 2020 +0100
@@ -93,6 +93,12 @@
 
   object Interrupt
   {
+    object ERROR
+    {
+      def unapply(exn: Throwable): Option[String] =
+        if (is_interrupt(exn)) Some(message(exn)) else user_message(exn)
+    }
+
     def apply(): Throwable = new InterruptedException("Interrupt")
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
diff -r c806eeb9138c -r b2bbe2e6575d src/Pure/Tools/build.scala
--- 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 =
         {