finally expose interrupt, similar to ML;
authorwenzelm
Sat, 04 Apr 2020 20:16:25 +0200
changeset 71688 220d19f3e074
parent 71687 f17be1db8381
child 71689 b3f738f12a9a
finally expose interrupt, similar to ML;
src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Sat Apr 04 20:06:15 2020 +0200
+++ b/src/Pure/Concurrent/standard_thread.scala	Sat Apr 04 20:16:25 2020 +0200
@@ -160,6 +160,7 @@
           super.interrupt()
         }
       }
+      Exn.Interrupt.expose()
     }
   }
 }