diff options
author | Samuel Mimram <smimram@debian.org> | 2008-01-03 16:26:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-01-03 16:26:12 +0000 |
commit | 2281410e38ef99d025ea77194585a9bc019fdaa9 (patch) | |
tree | 71ba76741c3ab6b752be876565dc34b0b0138dc5 /ide | |
parent | 4767d724d489a7ad67f696e9401e70b9f9ae2143 (diff) |
Imported Upstream version 8.1.pl3+dfsgupstream/8.1.pl3+dfsg
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coqide.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index fdc344e8..6cee46a6 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 10220 2007-10-12 13:25:54Z notin $ *) +(* $Id: coqide.ml 10229 2007-10-16 18:44:54Z notin $ *) open Preferences open Vernacexpr @@ -2856,10 +2856,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 @@ -2876,7 +2876,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 -> @@ -2942,7 +2942,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 -> |