author | wenzelm |
Wed, 11 Oct 2023 10:16:17 +0200 | |
changeset 78752 | 019cec83b49f |
parent 78747 | d03de7bc2137 |
child 78753 | f40b59292288 |
--- a/src/Pure/Concurrent/event_timer.ML Tue Oct 10 13:15:32 2023 +0200 +++ b/src/Pure/Concurrent/event_timer.ML Wed Oct 11 10:16:17 2023 +0200 @@ -118,7 +118,7 @@ (case next_event (Time.now (), ML_Heap.gc_now ()) requests of SOME (event, requests') => let - val _ = Exn.capture event (); + val _ = Exn.capture event (); (*sic!*) val state' = make_state (requests', status, manager); in SOME (true, state') end | NONE =>