From f67f84fc4831923aa9a2323b3a71c3a69fe61480 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:50:27 +0200
Subject: Use [method!] to override methods (warning 7)

---
 ide/wg_Notebook.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide/wg_Notebook.ml')

diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index 08d7d19833..0e5284c2f9 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
 
-- 
cgit v1.2.3