diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-20 15:16:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-20 15:19:44 +0200 |
| commit | c3ca30ca418ed0eca804d09fe6f1ff9d3ff0aa32 (patch) | |
| tree | 00643f67f2cd0a410b23c970933a590ffeb7d7da /lib | |
| parent | f6a4599b852a32351163eb272d14718e32b58cec (diff) | |
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.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/profile.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/lib/profile.ml b/lib/profile.ml index 78bf35621..0bc226a45 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 = |