diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-04 23:26:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-04 23:26:16 +0000 |
| commit | a05c335c2d38a5cf08bc0fda76d69a13e0ead040 (patch) | |
| tree | aaf61c9094d3ea292e3e247f4ca84d5461d2ebc3 /ide/preferences.ml | |
| parent | 34f8e2d160148e78abce969533739af8810d4347 (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.ml | 2 |
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 = |