diff options
| -rw-r--r-- | toplevel/vernac.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a59460bc54..d838954e6d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -239,14 +239,19 @@ let display_cmd_header loc com = str (" ["^cmd^"] ")); Pp.flush_all () +let is_profiling = + try ignore (Sys.getenv "CAMLRUNPARAM"); true + with Not_found -> false + let print_heap = let idx = ref 0 in fun () -> - let pid = Unix.getpid () in - let i = !idx in - let () = incr idx in - let filename = Printf.sprintf "heap.%i.%i" pid i in - Allocation_profiling.Global.dump_allocations_by_address ~filename + if is_profiling then + let pid = Unix.getpid () in + let i = !idx in + let () = incr idx in + let filename = Printf.sprintf "heap.%i.%i" pid i in + Allocation_profiling.Heap_snapshot.dump_allocators_of_major_heap_blocks ~filename let rec vernac_com verbosely checknav (loc,com) = let rec interp = function |