From db1719fbac08b5582fafddd4b76ef92f69cc5bc1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias 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. --- ide/coq.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide/coq.ml') diff --git a/ide/coq.ml b/ide/coq.ml index 65456d685..63986935a 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -152,7 +152,7 @@ let print_status = function let check_connection args = let lines = ref [] in let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote (coqtop_path ()) ^ " -batch -ideslave " ^ argstr in + let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in let cmd = requote cmd in try let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in @@ -377,7 +377,7 @@ let spawn_handle args respawner feedback_processor = else "on" in - let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in + let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: args) in let env = match !ideslave_coqtop_flags with | None -> None -- cgit v1.2.3