changeset 69826 | 1bea05713dde |
parent 67000 | 1698e9ccef2d |
child 71692 | f8e52c0152fe |
--- a/src/Pure/Concurrent/timeout.ML Wed Feb 20 21:20:30 2019 +0100 +++ b/src/Pure/Concurrent/timeout.ML Wed Feb 20 21:54:52 2019 +0100 @@ -23,7 +23,7 @@ val start = Time.now (); val request = - Event_Timer.request (start + timeout) + Event_Timer.request {physical = false} (start + timeout) (fn () => Standard_Thread.interrupt_unsynchronized self); val result = Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();