aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/preferences.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-04 23:26:16 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-04 23:26:16 +0000
commita05c335c2d38a5cf08bc0fda76d69a13e0ead040 (patch)
treeaaf61c9094d3ea292e3e247f4ca84d5461d2ebc3 /ide/preferences.ml
parent34f8e2d160148e78abce969533739af8810d4347 (diff)
Display Menu now called View Menu (in CoqIDE preferences).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16018 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r--ide/preferences.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 3a2204601..ed4f4cd1f 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -699,7 +699,7 @@ let configure ?(apply=(fun () -> ())) () =
~allow:the_valid_mod
~f:(fun l -> current.modifier_for_display <- mod_list_to_str l)
~help:help_string
- "Modifiers for Display Menu"
+ "Modifiers for View Menu"
(str_to_mod_list current.modifier_for_display)
in
let modifiers_valid =