diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 0a83e609b..1da8b3157 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -105,10 +105,5 @@ val configure : ?apply:(unit -> unit) -> unit -> unit (* Hooks *) val refresh_editor_hook : (unit -> unit) ref -val refresh_style_hook : (unit -> unit) ref -val refresh_language_hook : (unit -> unit) ref -val refresh_toolbar_hook : (unit -> unit) ref -val resize_window_hook : (unit -> unit) ref -val refresh_tabs_hook : (unit -> unit) ref val use_default_doc_url : string |