clarified comments;
authorwenzelm
Wed, 11 Oct 2023 10:16:17 +0200
changeset 78752 019cec83b49f
parent 78747 d03de7bc2137
child 78753 f40b59292288
clarified comments;
src/Pure/Concurrent/event_timer.ML
--- 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 =>