From 57030f36d88800004a5bf9d0581d23f60daddad9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 16 Feb 2021 11:00:47 +0100
Subject: [coqtop] be verbose only in interactive mode

---
 toplevel/coqtop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index caf86ef870..c0d2bab218 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -174,7 +174,7 @@ let init_toploop opts stm_opts injections =
   state
 
 let coqtop_init ({ run_mode; color_mode }, async_opts) injections ~opts =
-  if run_mode = Batch then Flags.quiet := true;
+  if run_mode != Interactive then Flags.quiet := true;
   init_color (if opts.config.print_emacs then `EMACS else color_mode);
   Flags.if_verbose print_header ();
   init_toploop opts async_opts injections
-- 
cgit v1.2.3