diff options
author | 2012-12-19 00:05:16 +0000 | |
---|---|---|
committer | 2012-12-19 00:05:16 +0000 | |
commit | 7a30e5bbcfb2dc3e7b7bf0cf2cd4e27eab31dcfb (patch) | |
tree | b53177b532f65d690d70af239b8fb6e22283b818 /ide/preferences.ml | |
parent | ecc9544f651aaa8ea0853206f290f2e15d5dd21e (diff) |
GtkData.set_default_modifiers and no access to <primary> in lablgtk -> unsuable Coqide under MacOS
makes Command not working on MacOS and consequently breaks all default shortcuts 'o' opens a file 'w' close the buffer ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16103 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r-- | ide/preferences.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 3116be1af..85c569015 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -341,7 +341,6 @@ let load_pref () = (fun v -> np.modifier_for_display <- v); set_hd "modifiers_valid" (fun v -> - let () = GtkData.AccelGroup.set_default_mod_mask (Some (str_to_mod_list v)) in np.modifiers_valid <- v); set_command_with_pair_compat "cmd_browse" (fun v -> np.cmd_browse <- v); set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v); @@ -705,7 +704,6 @@ let configure ?(apply=(fun () -> ())) () = let modifiers_valid = modifiers ~f:(fun l -> - let () = GtkData.AccelGroup.set_default_mod_mask (Some l) in current.modifiers_valid <- mod_list_to_str l) "Allowed modifiers" the_valid_mod |