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/project_file.ml4 | |
| 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/project_file.ml4')
0 files changed, 0 insertions, 0 deletions