From 5a6032ff8e8aec41bd78f3939142e0b6e0527b5d Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 16 Oct 2007 18:44:54 +0000 Subject: Correction d'un bug de l'appel à make via Coqide git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10229 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqide.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 805246f48e..cf18d0ae4e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2863,10 +2863,10 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); | None -> !flash_info "Active buffer has no name" | Some f -> - let s,res = run_command - av#insert_message - (!current.cmd_coqc ^ " " ^ (Filename.quote f)) - in + let cmd = !current.cmd_coqc ^ " -I " + ^ (Filename.quote (Filename.dirname f)) + ^ " " ^ (Filename.quote f) in + let s,res = run_command av#insert_message cmd in if s = Unix.WEXITED 0 then !flash_info (f ^ " successfully compiled") else begin @@ -2883,7 +2883,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/Make Menu *) let make_f () = - let v = get_active_view () in + let v = get_current_view () in let av = out_some v.analyzed_view in match av#filename with | None -> @@ -2896,7 +2896,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); save_f (); *) av#insert_message "Command output:\n"; - let s,res = run_command av#insert_message !current.cmd_make in + let s,res = run_command av#insert_message cmd in last_make := res; last_make_index := 0; !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") @@ -2950,7 +2950,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/CoqMakefile Menu*) let coq_makefile_f () = - let v = get_active_view () in + let v = get_current_view () in let av = out_some v.analyzed_view in match av#filename with | None -> -- cgit v1.2.3