Merge PR #10612: Fix feedback levels

Ack-by: ejgallego
Reviewed-by: gares

1 files changed, 2 insertions, 2 deletions

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