From 6bc9ef56c5833ee81d7298ab0c52146ad775e2a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 2 Aug 2019 16:47:49 +0200
Subject: Make sure that all query commands return a notice (not an info)
 feedback

As documented in the feedback API.
---
 plugins/ltac/profile_ltac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/profile_ltac.ml')

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9d46bbc74e..fe5ebf1172 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -417,7 +417,7 @@ let get_timer name =
 let finish_timing ~prefix name =
   let tend = System.get_time () in
   let tstart = get_timer name in
-  Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+  Feedback.msg_notice(str prefix ++ pr_opt str name ++ str " ran for " ++
                     System.fmt_time_difference tstart tend)
 
 (* ******************** *)
@@ -431,7 +431,7 @@ let print_results_filter ~cutoff ~filter =
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-  Feedback.msg_info (to_string ~cutoff ~filter results)
+  Feedback.msg_notice (to_string ~cutoff ~filter results)
 ;;
 
 let print_results ~cutoff =
-- 
cgit v1.2.3