diff options
| author | Hugo Herbelin | 2018-10-29 16:03:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-10 12:03:18 +0200 |
| commit | 1503ab7737efb29bc17c22a242e9f66be50a0762 (patch) | |
| tree | 7fded573e8490c0c6debf1bf9c65aeec34d00b73 | |
| parent | 5b13384e1b5bd4f11f22036f4eb83c63a4ae88c2 (diff) | |
Making a bit clearer that CoqIDE modifier menu is for global modifier change.
Indeed, one can change each item locally, but the preference menu is
only for changing the modifiers of a whole menu at once.
| -rw-r--r-- | ide/preferences.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index ed51eb0b91..52122441a1 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -898,19 +898,19 @@ let configure ?(apply=(fun () -> ())) parent = in let project_file_name = pstring "Default name for project file" project_file_name in let modifier_for_tactics = - pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics + pmodifiers "Global change of modifiers for Tactics Menu" modifier_for_tactics in let modifier_for_templates = - pmodifiers "Modifiers for Templates Menu" modifier_for_templates + pmodifiers "Global change of modifiers for Templates Menu" modifier_for_templates in let modifier_for_navigation = - pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation + pmodifiers "Global change of modifiers for Navigation Menu" modifier_for_navigation in let modifier_for_display = - pmodifiers "Modifiers for View Menu" modifier_for_display + pmodifiers "Global change of modifiers for View Menu" modifier_for_display in let modifier_for_queries = - pmodifiers "Modifiers for Queries Menu" modifier_for_queries + pmodifiers "Global change of modifiers for Queries Menu" modifier_for_queries in let modifiers_valid = pmodifiers ~all:true "Allowed modifiers" modifiers_valid |