From d5af8a969cfbd32484b4939bfeff153c86fc2fe2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 10 Sep 2019 15:16:29 +0200
Subject: CoqIDE: removing option contextual menu on goal, inactive since
 2da5db43c.

---
 ide/preferences.ml  | 7 +------
 ide/preferences.mli | 1 -
 2 files changed, 1 insertion(+), 7 deletions(-)

(limited to 'ide')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 2cc98e6927..7b667027fc 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -379,9 +379,6 @@ let text_font =
 let show_toolbar =
   new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool)
 
-let contextual_menus_on_goal =
-  new preference ~name:["contextual_menus_on_goal"] ~init:true ~repr:Repr.(bool)
-
 let window_width =
   new preference ~name:["window_width"] ~init:800 ~repr:Repr.(int)
 
@@ -982,9 +979,7 @@ let configure ?(apply=(fun () -> ())) parent =
       cmd_browse#get
   in
 
-  let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in
-
-  let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
+  let misc = [stop_before;reset_on_tab_switch;
               vertical_tabs;opposite_tabs] in
 
 (*
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 6da6228545..4b04326cec 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -79,7 +79,6 @@ val cmd_browse : string preference
 val cmd_editor : string preference
 val text_font : string preference
 val show_toolbar : bool preference
-val contextual_menus_on_goal : bool preference
 val window_width : int preference
 val window_height : int preference
 val auto_complete : bool preference
-- 
cgit v1.2.3