# HG changeset patch
# User wenzelm
# Date 1601384737 -7200
# Node ID b8708212bdd5ad9dbffd7372bc00c16d41c47317
# Parent  6916b48b375c3b8b8c959784d748dd06dc286466
clarified message;

diff -r 6916b48b375c -r b8708212bdd5 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Sep 29 13:52:01 2020 +0200
+++ b/src/Pure/General/exn.scala	Tue Sep 29 15:05:37 2020 +0200
@@ -93,7 +93,7 @@
 
   object Interrupt
   {
-    def apply(): Throwable = new InterruptedException
+    def apply(): Throwable = new InterruptedException("Interrupt")
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
     def dispose() { Thread.interrupted }