diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 7ed6a40bdb..8745c2ae91 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -8,8 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val lang_manager : GSourceView2.source_language_manager -val style_manager : GSourceView2.source_style_scheme_manager +val lang_manager : GSourceView3.source_language_manager +val style_manager : GSourceView3.source_style_scheme_manager type project_behavior = Ignore_args | Append_args | Subst_args type inputenc = Elocale | Eutf8 | Emanual of string @@ -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 @@ -110,6 +108,6 @@ val load_pref : unit -> unit val configure : ?apply:(unit -> unit) -> GWindow.window -> unit val stick : 'a preference -> - (#GObj.widget as 'obj) -> ('a -> unit) -> unit + < connect : #GObj.widget_signals ; .. > -> ('a -> unit) -> unit val use_default_doc_url : string |