aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--test-suite/Makefile2
-rw-r--r--tools/fake_ide.ml20
2 files changed, 17 insertions, 5 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index a88fb6bc6..beb80a3df 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -446,7 +446,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
@echo "TEST $<"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(BIN)fake_ide $< "$(BIN)coqtop -coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
+ $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
if [ $$? = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 258633d29..a9da27ba2 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -297,12 +297,24 @@ let main =
(Sys.Signal_handle
(fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
- let coqtop_name, coqtop_args, input_file = match Sys.argv with
- | [| _; f |] -> (if Sys.os_type = "Unix" then "coqtop" else "coqtop.exe"),
- Array.of_list def_args, f
+ let coqtop_name = (* from ide/ideutils.ml *)
+ let prog_name = "fake_ide" in
+ let len_prog_name = String.length prog_name in
+ let fake_ide_path = Sys.executable_name in
+ let fake_ide_path_len = String.length fake_ide_path in
+ let pos = fake_ide_path_len - len_prog_name in
+ let rex = Str.regexp_string prog_name in
+ try
+ let i = Str.search_backward rex fake_ide_path pos in
+ String.sub fake_ide_path 0 i ^ "coqtop" ^
+ String.sub fake_ide_path (i + len_prog_name)
+ (fake_ide_path_len - i - len_prog_name)
+ with Not_found -> assert false in
+ let coqtop_args, input_file = match Sys.argv with
+ | [| _; f |] -> Array.of_list def_args, f
| [| _; f; ct |] ->
let ct = Str.split (Str.regexp " ") ct in
- List.hd ct, Array.of_list (def_args @ List.tl ct), f
+ Array.of_list (def_args @ ct), f
| _ -> usage () in
let inc = if input_file = "-" then stdin else open_in input_file in
let coq =