aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 869f6bb93..aab20650a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -549,6 +549,7 @@ let parse_args arglist =
else native_compiler := true
|"-notop" -> unset_toplevel_name ()
|"-output-context" -> output_context := true
+ |"-profile-ltac" -> Flags.profile_ltac := true
|"-q" -> no_load_rc ()
|"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false
|"-quick" -> Flags.compilation_mode := BuildVio