diff options
| -rw-r--r-- | otherlibs/threads/pervasives.ml | 4 | ||||
| -rw-r--r-- | stdlib/pervasives.ml | 3 |
2 files changed, 7 insertions, 0 deletions
diff --git a/otherlibs/threads/pervasives.ml b/otherlibs/threads/pervasives.ml index 6cc15911e..91c9b8651 100644 --- a/otherlibs/threads/pervasives.ml +++ b/otherlibs/threads/pervasives.ml @@ -477,3 +477,7 @@ let do_at_exit () = (!exit_function) () let exit retcode = do_at_exit (); sys_exit retcode + +external register_named_value: string -> 'a -> unit = "register_named_value" + +let _ = register_named_value "Pervasives.do_at_exit" do_at_exit diff --git a/stdlib/pervasives.ml b/stdlib/pervasives.ml index 8657d6959..5f196a4b4 100644 --- a/stdlib/pervasives.ml +++ b/stdlib/pervasives.ml @@ -366,3 +366,6 @@ let exit retcode = do_at_exit (); sys_exit retcode +external register_named_value: string -> 'a -> unit = "register_named_value" + +let _ = register_named_value "Pervasives.do_at_exit" do_at_exit |