From c3ca30ca418ed0eca804d09fe6f1ff9d3ff0aa32 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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.
---
 toplevel/coqtop.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 08c235023..d79257b5c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -613,6 +613,7 @@ let parse_args arglist =
   with any -> fatal_error any
 
 let init_toplevel arglist =
+  Profile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   let init_feeder = Feedback.add_feeder coqtop_init_feed in
-- 
cgit v1.2.3