From c3ca30ca418ed0eca804d09fe6f1ff9d3ff0aa32 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Jul 2017 15:16:05 +0200
Subject: Also a less intrusive Profile.init_profile.

Calling it only when there is something to profile, or when profiling
is explicitly required with the profile flags, so that profiling in
plugins is possible.
---
 lib/profile.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/profile.ml b/lib/profile.ml
index 78bf35621a..0bc226a450 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -85,6 +85,9 @@ let init_alloc = ref 0.0
 let reset_profile () = List.iter reset_record !prof_table
 
 let init_profile () =
+  (* We test Flags.profile as a way to support declaring profiled
+     functions in plugins *)
+  if !prof_table <> [] || Flags.profile then begin
   let outside = create_record () in
   stack := [outside];
   last_alloc := get_alloc ();
@@ -92,6 +95,7 @@ let init_profile () =
   init_time := get_time ();
   outside.tottime <- - !init_time;
   outside.owntime <- - !init_time
+  end
 
 let ajoute n o =
   o.owntime <- o.owntime + n.owntime;
@@ -358,9 +362,6 @@ let declare_profile name =
   prof_table := (name,e)::!prof_table;
   e
 
-(* Default initialization, may be overridden *)
-let _ = init_profile ()
-
 (******************************)
 (* Entry points for profiling *)
 let profile1 e f a =
-- 
cgit v1.2.3