aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d09171bc8..515552fe7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -614,6 +614,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