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.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'lib/flags.mli')

diff --git a/lib/flags.mli b/lib/flags.mli
index ea50d41da9..a0ff0f55ea 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,9 @@ val xml_export : bool ref
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
+val feedback_goals : bool ref
+
+
 val time : bool ref
 
 val we_are_parsing : bool ref
-- 
cgit v1.2.3