diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 1 |
1 files changed, 0 insertions, 1 deletions
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 |