From 2a805fd99b96746dbfe381d64cd7eaba84fdca79 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jul 2014 15:59:44 +0200
Subject: Feedback: LoadedFile + Goals

LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
---
 toplevel/coqtop.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0ccb6faafd..be63db391d 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 ())
-- 
cgit v1.2.3