diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:29:43 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:29:43 +0200 |
| commit | 5874843ea8e1ca82f8b1b646022582309b7fe24c (patch) | |
| tree | 3bd4172fd68dd06c2c3d1a20d697e0b7cfbacc89 /ide/preferences.mli | |
| parent | 6cc27d2ca57a5d2fedfa52d8b44c37c60ccb6988 (diff) | |
Add user-created queries to CoqIDE.
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 |