diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 1733091a5..ebcff2080 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -95,6 +95,7 @@ val spaces_instead_of_tabs : bool preference val tab_length : int preference val highlight_current_line : bool preference val nanoPG : bool preference +val user_queries : (string * string) list preference val save_pref : unit -> unit val load_pref : unit -> unit |