From a4cfaa49b5bac5cf437403ec021fcd7325fc1554 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 29 Oct 2013 17:11:09 +0000
Subject: Profile only when CAMLRUNPARAM is set.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16950 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernac.ml | 15 ++++++++++-----
 1 file 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
-- 
cgit v1.2.3