# HG changeset patch
# User wenzelm
# Date 1378892067 -7200
# Node ID 9b0af3298cda647647a22e8dd375d6ac5648add2
# Parent  3120c2ce5a75fc89e8941acdfc1e808c6a11e039
tuned comment;

diff -r 3120c2ce5a75 -r 9b0af3298cda src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Wed Sep 11 11:08:48 2013 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Wed Sep 11 11:34:27 2013 +0200
@@ -25,7 +25,7 @@
 fun fork interrupts body =
   Thread.fork (fn () =>
     exception_trace (fn () =>
-      body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
+      body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
     attributes interrupts);
 
 fun join thread =