diff options
| -rw-r--r-- | ide/preferences.ml | 7 | ||||
| -rw-r--r-- | ide/preferences.mli | 1 |
2 files changed, 1 insertions, 7 deletions
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 |