diff options
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 8525d731b..0b7adf33f 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -12,7 +12,6 @@ val boot : bool ref val batch_mode : bool ref -val ide_slave_mode : bool ref val coq_slave_mode : int ref val coq_slaves_number : int ref @@ -27,6 +26,7 @@ val term_quality : bool ref val xml_export : bool ref val ide_slave : bool ref +val ide_slave_socket : (string * int) option ref val time : bool ref |