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