# HG changeset patch # User wenzelm # Date 1369062633 -7200 # Node ID 5534ec8b90a91955a7f23ff339b2df590a0c1aa7 # Parent 573e80625c78d667a982487fcf663c88cd932947 tuned; diff -r 573e80625c78 -r 5534ec8b90a9 src/Pure/Concurrent/time_limit.ML --- a/src/Pure/Concurrent/time_limit.ML Mon May 20 16:17:56 2013 +0200 +++ b/src/Pure/Concurrent/time_limit.ML Mon May 20 17:10:33 2013 +0200 @@ -32,8 +32,7 @@ in if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test) then raise TimeOut - else if Exn.is_interrupt_exn test then Exn.interrupt () - else Exn.release result + else (Exn.release test; Exn.release result) end); end;