diff options
| -rw-r--r-- | otherlibs/systhreads/pervasives.ml | 10 | ||||
| -rw-r--r-- | otherlibs/threads/pervasives.ml | 10 |
2 files changed, 12 insertions, 8 deletions
diff --git a/otherlibs/systhreads/pervasives.ml b/otherlibs/systhreads/pervasives.ml index 7ab2103a8..404db9ca5 100644 --- a/otherlibs/systhreads/pervasives.ml +++ b/otherlibs/systhreads/pervasives.ml @@ -362,10 +362,12 @@ external sys_exit : int -> 'a = "sys_exit" let exit_function = ref (fun () -> flush stdout; flush stderr) -let exit retcode = - (!exit_function)(); - sys_exit retcode - let at_exit f = let g = !exit_function in exit_function := (fun () -> f(); g()) + +let do_at_exit () = (!exit_function) () + +let exit retcode = + do_at_exit (); + sys_exit retcode diff --git a/otherlibs/threads/pervasives.ml b/otherlibs/threads/pervasives.ml index 71a743f83..7dfcdd4fd 100644 --- a/otherlibs/threads/pervasives.ml +++ b/otherlibs/threads/pervasives.ml @@ -372,10 +372,12 @@ external sys_exit : int -> 'a = "sys_exit" let exit_function = ref (fun () -> flush stdout; flush stderr) -let exit retcode = - (!exit_function)(); - sys_exit retcode - let at_exit f = let g = !exit_function in exit_function := (fun () -> f(); g()) + +let do_at_exit () = (!exit_function) () + +let exit retcode = + do_at_exit (); + sys_exit retcode |