From 4bc9529ece085441121678a07e4b269c7633471c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 5 Feb 2018 04:02:27 +0100
Subject: [ide] Localize a IDE-specific flag.

---
 lib/flags.ml  | 2 --
 lib/flags.mli | 1 -
 2 files changed, 3 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 01361dad5..415e4399a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -56,10 +56,8 @@ let in_toplevel = ref false
 let profile = false
 
 let ide_slave = ref false
-let ideslave_coqtop_flags = ref None
 
 let raw_print = ref false
-
 let univ_print = ref false
 
 let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 33d281798..c82410f07 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -33,7 +33,6 @@ val profile : bool
 
 (* -ide_slave: printing will be more verbose, will affect stm caching *)
 val ide_slave : bool ref
-val ideslave_coqtop_flags : string option ref
 
 (* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
-- 
cgit v1.2.3