diff options
Diffstat (limited to 'stdlib/gc.ml')
| -rw-r--r-- | stdlib/gc.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/stdlib/gc.ml b/stdlib/gc.ml index a6a874eaa..9dcc5ae19 100644 --- a/stdlib/gc.ml +++ b/stdlib/gc.ml @@ -70,3 +70,5 @@ let print_stat c = let allocated_bytes () = let (mi, ma, pro) = counters () in (mi + ma - pro) * (Sys.word_size / 8) ;; + +external finalise : ('a -> unit) -> 'a -> unit = "final_register";; |