diff options
| -rw-r--r-- | ide/preferences.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 1dfa699808..a8be10de98 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -120,9 +120,9 @@ let (current:pref ref) = "auto with *"; "intuition" ]; modifier_for_navigation = [`CONTROL; `MOD1]; - modifier_for_templates = [`MOD4]; + modifier_for_templates = [`CONTROL; `SHIFT]; modifier_for_tactics = [`CONTROL; `MOD1]; - modifiers_valid = [`SHIFT; `CONTROL; `MOD1; `MOD4]; + modifiers_valid = [`SHIFT; `CONTROL; `MOD1]; cmd_browse = Options.browser_cmd_fmt; |