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 0ccb6faaf..be63db391 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -360,6 +360,7 @@ let parse_args arglist =
|"-compile-verbose" -> add_compile true (next ())
|"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
|"-feedback-glob" -> Dumpglob.feedback_glob ()
+ |"-feedback-goals" -> Flags.feedback_goals := true
|"-exclude-dir" -> exclude_search_in_dirname (next ())
|"-init-file" -> set_rcfile (next ())
|"-inputstate"|"-is" -> set_inputstate (next ())