Merge branch 'master'.

5 files changed, 8 insertions, 10 deletions

diff --git a/ide/.merlin b/ide/.merlin
index 3f3d9d275d..953b5dce4c 100644
--- a/ide/.merlin
+++ b/ide/.merlin
@@ -1,4 +1,4 @@
-PKG lablgtk2.sourceview2
+PKG unix laglgtk2 lablgtk2.sourceview2
 
 S utils
 B utils
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 8fc5547ece..4967ddb753 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -393,7 +393,8 @@ let init =
              Stm.add false ~ontop:(Stm.get_current_state ())
                0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
            else Stm.get_current_state (), `NewTip in
-         Stm.set_compilation_hints file;
+         if Filename.check_suffix file ".v" then
+           Stm.set_compilation_hints file;
          Stm.finish ();
          initial_id
    end
diff --git a/ide/interface.mli b/ide/interface.mli
index 2a9b8b241f..123cac6c22 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -139,7 +139,7 @@ type add_rty = state_id * ((unit, state_id) union * string)
     [Inr (start,(stop,tip))] if [id] is in a zone that can be focused.
     In that case the zone is delimited by [start] and [stop] while [tip]
     is the new document [tip].  Edits made by subsequent [add] are always
-    performend on top of [id]. *)
+    performed on top of [id]. *)
 type edit_at_sty = state_id
 type edit_at_rty = (unit, state_id * (state_id * state_id)) union
 
@@ -153,7 +153,7 @@ type query_rty = string
 type goals_sty = unit
 type goals_rty = goals option
 
-(** Retrieve the list of unintantiated evars in the current proof. [None] if no
+(** Retrieve the list of uninstantiated evars in the current proof. [None] if no
     proof is in progress. *)
 type evars_sty = unit
 type evars_rty = evar list option
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 64327d74f5..f0fd45d77f 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -468,7 +468,7 @@ let create_tag name default =
   let iter table =
     let tag = GText.tag ~name () in
     table#add tag#as_tag;
-    pref#connect#changed (fun _ -> set_tag tag);
+    ignore (pref#connect#changed (fun _ -> set_tag tag));
     set_tag tag;
   in
   List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
@@ -918,7 +918,7 @@ let configure ?(apply=(fun () -> ())) () =
   in
   let doc_url =
     let predefined = [
-      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";""]);
+      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]);
       Coq_config.wwwrefman;
       use_default_doc_url
     ] in
@@ -931,7 +931,7 @@ let configure ?(apply=(fun () -> ())) () =
       doc_url#get in
   let library_url =
     let predefined = [
-      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]);
+      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]);
       Coq_config.wwwstdlib
     ] in
     combo
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index aecb317bcb..5f82a8898b 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -816,7 +816,6 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "workerstatus", [ns] ->
        let n, s = to_pair to_string to_string ns in
        WorkerStatus(n,s)
-  | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
   | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
   | "filedependency", [from; dep] ->
       FileDependency (to_option to_string from, to_string dep)
@@ -849,8 +848,6 @@ let of_feedback_content = function
   | WorkerStatus(n,s) ->
       constructor "feedback_content" "workerstatus"
         [of_pair of_string of_string (n,s)]
-  | Goals (loc,s) ->
-      constructor "feedback_content" "goals" [of_loc loc;of_string s]
   | Custom (loc, name, x) ->
       constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
   | FileDependency (from, depends_on) ->