diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:40:33 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:40:33 +0200 |
| commit | c6d5f9c39b3e12f58745c22eade90d34548b6283 (patch) | |
| tree | e42a27483494c7f03844f657609c9ff691f8603d /ide/preferences.mli | |
| parent | abd469790c2e144f693e1b21c5cdc03aee178e6d (diff) | |
Add an option to configure the modifier for Queries.
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 ebcff2080..426b0a328 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -65,6 +65,7 @@ val modifier_for_navigation : string preference val modifier_for_templates : string preference val modifier_for_tactics : string preference val modifier_for_display : string preference +val modifier_for_queries : string preference val modifiers_valid : string preference val cmd_browse : string preference val cmd_editor : string preference |