Use [method!] to override methods (warning 7)

4 files changed, 8 insertions, 8 deletions

diff --git a/ide/preferences.ml b/ide/preferences.ml
index e1fc4005b..9fe9c6337 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -360,7 +360,7 @@ object
     ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string)
     as super
 
-  method set v =
+  method! set v =
     if not (Flags.is_standard_doc_url v) &&
       v <> use_default_doc_url &&
       (* Extra hack to support links to last released doc version *)
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml
index 3d1b63dfa..cbc34462e 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/wg_Detachable.ml
@@ -26,8 +26,8 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) =
     val mutable attached_cb = (fun _ -> ())
 
     method child = frame#child
-    method add = frame#add
-    method pack ?from ?expand ?fill ?padding w =
+    method! add = frame#add
+    method! pack ?from ?expand ?fill ?padding w =
       if frame#all_children = [] then self#add w
       else raise (Invalid_argument "detachable#pack")
 
diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index 08d7d1983..0e5284c2f 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/wg_Notebook.ml
@@ -50,7 +50,7 @@ object(self)
 
   method pages = term_list
 
-  method remove_page index =
+  method! remove_page index =
     term_list <- Util.List.filteri (fun i x -> if i = index then kill_page x; i <> index) term_list;
     super#remove_page index
 
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 7c058febd..7430f07d4 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -301,28 +301,28 @@ object (self)
       ~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT
 
   (* HACK: missing gtksourceview features *)
-  method right_margin_position =
+  method! right_margin_position =
     let prop = {
       Gobject.name = "right-margin-position";
       conv = Gobject.Data.int;
     } in
     Gobject.get prop obj
 
-  method set_right_margin_position pos =
+  method! set_right_margin_position pos =
     let prop = {
       Gobject.name = "right-margin-position";
       conv = Gobject.Data.int;
     } in
     Gobject.set prop obj pos
 
-  method show_right_margin =
+  method! show_right_margin =
     let prop = {
       Gobject.name = "show-right-margin";
       conv = Gobject.Data.boolean;
     } in
     Gobject.get prop obj
 
-  method set_show_right_margin show =
+  method! set_show_right_margin show =
     let prop = {
       Gobject.name = "show-right-margin";
       conv = Gobject.Data.boolean;