diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 7ed6a40bdb..cf2265781c 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -74,8 +74,6 @@ val modifiers_valid : string preference val cmd_browse : string preference val cmd_editor : string preference val text_font : string preference -val doc_url : string preference -val library_url : string preference val show_toolbar : bool preference val contextual_menus_on_goal : bool preference val window_width : int preference |