From 1503ab7737efb29bc17c22a242e9f66be50a0762 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 29 Oct 2018 16:03:44 +0100
Subject: 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.
---
 ide/preferences.ml | 10 +++++-----
 1 file 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
-- 
cgit v1.2.3