From 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:03:54 +0200
Subject: Remove uses of [Flags.make_silent]

---
 ide/ide_slave.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index dbfe4256b3..966a94da91 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -505,7 +505,7 @@ let rec parse = function
 
 let () = Coqtop.toploop_init := (fun args ->
         let args = parse args in
-        Flags.make_silent true;
+        Flags.quiet := true;
         CoqworkmgrApi.(init Flags.High);
         args)
 
-- 
cgit v1.2.3