author | wenzelm |
Wed, 11 Sep 2013 11:34:27 +0200 | |
changeset 53527 | 9b0af3298cda |
parent 53526 | 3120c2ce5a75 |
child 53528 | 129bd52a5e5f |
--- 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 =