From 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Tue, 25 Apr 2017 14:03:54 +0200
Subject: Remove uses of [Flags.make_silent]

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

(limited to 'checker/checker.ml')

diff --git a/checker/checker.ml b/checker/checker.ml
index 57e1806cf..5cadfe7b9 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -354,7 +354,7 @@ let parse_args argv =
     | "-norec" :: [] -> usage ()
 
     | "-silent" :: rem ->
-        Flags.make_silent true; parse rem
+        Flags.quiet := true; parse rem
 
     | s :: _ when s<>"" && s.[0]='-' ->
         fatal_error (str "Unknown option " ++ str s) false
-- 
cgit v1.2.3