From 3ccc9a89de9a2d5b81dae82c7815ba077f998135 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Nov 2018 13:22:43 +0100
Subject: CoqIDE: remove obselete menu item "Complete word".

This was obsolete since new completion in 945d7db9 (then a07359f6).
---
 ide/coqide.ml    | 2 --
 ide/coqide_ui.ml | 1 -
 2 files changed, 3 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 4190f43680..60ba9b5351 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1004,8 +1004,6 @@ let build_ui () =
     item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP
       ~accel:"<Shift>F3"
       ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ()));
-    item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash"
-      ~callback:(fun _ -> ());
     item "External editor" ~label:"External editor" ~stock:`EDIT
       ~callback:External.editor;
     item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 91c529932f..c994898a4f 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -60,7 +60,6 @@ let init () =
 \n    <menuitem action='Find' />\
 \n    <menuitem action='Find Next' />\
 \n    <menuitem action='Find Previous' />\
-\n    <menuitem action='Complete Word' />\
 \n    <separator />\
 \n    <menuitem action='External editor' />\
 \n    <separator />\
-- 
cgit v1.2.3