diff options
| author | Hugo Herbelin | 2019-05-08 13:01:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:26 +0200 |
| commit | 26b7e819746a6b36d0e22181f64549c503fe0481 (patch) | |
| tree | 3cbbd7b167ffb488e2b0cbe1508a67ad5c8e22c7 | |
| parent | fe5389542af2d9b6e8d964bbc2c10e997af409fe (diff) | |
Function print_memory_stat: getting rid of a mutable.
| -rw-r--r-- | toplevel/coqtop.ml | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 22d293129e..2f2cebe074 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -30,23 +30,18 @@ let print_header () = Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -let memory_stat = ref false let print_memory_stat () = - begin (* -m|--memory from the command-line *) - if !memory_stat then - Feedback.msg_notice - (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()); - end; - begin - (* operf-macro interface: - https://github.com/OCamlPro/operf-macro *) - try - let fn = Sys.getenv "OCAML_GC_STATS" in - let oc = open_out fn in - Gc.print_stat oc; - close_out oc - with _ -> () - end + (* -m|--memory from the command-line *) + Feedback.msg_notice + (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()); + (* operf-macro interface: + https://github.com/OCamlPro/operf-macro *) + try + let fn = Sys.getenv "OCAML_GC_STATS" in + let oc = open_out fn in + Gc.print_stat oc; + close_out oc + with _ -> () let interp_set_option opt v old = let open Goptions in |