clarified message;
authorwenzelm
Tue, 29 Sep 2020 15:05:37 +0200
changeset 72335 b8708212bdd5
parent 72334 6916b48b375c
child 72336 41a4352c5240
clarified message;
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 }