diff options
author | 2015-09-21 10:35:56 +0200 | |
---|---|---|
committer | 2015-09-21 10:35:56 +0200 | |
commit | 0ac3a2f4de0dc02b973c9f5d59b3c0a97f888141 (patch) | |
tree | 45293430f0da0f1df26a5054fe852b27e54110b1 /ide/wg_Command.mli | |
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/wg_Command.mli')
0 files changed, 0 insertions, 0 deletions