From db1719fbac08b5582fafddd4b76ef92f69cc5bc1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 28 Feb 2018 03:26:12 +0100
Subject: [ide] Remove special option `-ideslave`

This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
---
 lib/flags.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'lib/flags.mli')

diff --git a/lib/flags.mli b/lib/flags.mli
index 17776d68a..02d8a3adc 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -52,9 +52,6 @@ val in_toplevel : bool ref
 
 val profile : bool
 
-(* -ide_slave: printing will be more verbose, will affect stm caching *)
-val ide_slave : bool ref
-
 (* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
 
-- 
cgit v1.2.3