diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-21 10:35:56 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-21 10:35:56 +0200 |
| commit | 0ac3a2f4de0dc02b973c9f5d59b3c0a97f888141 (patch) | |
| tree | 45293430f0da0f1df26a5054fe852b27e54110b1 /ide | |
| parent | b3bd2696c31ad2cb544f3436ddb5a237fe7fa6fe (diff) | |
Change the default modifiers for navigation. (Fix bug #4295)
On most systems (including Windows, according to the bug report), shortcuts
Ctrl+Alt+Arrows are preempted by the window manager by default. So don't
use them for navigation in Coqide by default. Note that this change only
has an impact when installing on a fresh system; it won't change anything
for existing users.
Diffstat (limited to 'ide')
| -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 1bd9f587c..90862d064 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -190,7 +190,7 @@ let current = { automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ]; - modifier_for_navigation = "<Control><Alt>"; + modifier_for_navigation = "<Control>"; modifier_for_templates = "<Control><Shift>"; modifier_for_tactics = "<Control><Alt>"; modifier_for_display = "<Alt><Shift>"; |