summaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-01-03 16:26:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2008-01-03 16:26:12 +0000
commit2281410e38ef99d025ea77194585a9bc019fdaa9 (patch)
tree71ba76741c3ab6b752be876565dc34b0b0138dc5 /ide
parent4767d724d489a7ad67f696e9401e70b9f9ae2143 (diff)
Imported Upstream version 8.1.pl3+dfsgupstream/8.1.pl3+dfsg
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide.ml14
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 ->