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.
---
 library/goptions.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/goptions.ml b/library/goptions.ml
index c7024ca81d..0973944fb5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -398,9 +398,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+        Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+        Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in
-- 
cgit v1.2.3