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
---
 lib/flags.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 36bb447ae9..9dd65db6dc 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -70,6 +70,8 @@ let xml_export = ref false
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
+let feedback_goals = ref false
+
 let time = ref false
 
 let raw_print = ref false
-- 
cgit v1.2.3