aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/preferences.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r--ide/preferences.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 499fac6f1..f10f3e503 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -199,7 +199,8 @@ let save_pref () =
Config_lexer.print_file pref_file
let load_pref () =
- (try GtkData.AccelMap.load accel_file with _ -> ());
+ GtkData.AccelMap.load (Filename.concat !Minilib.coqlib "ide/default_accel_map");
+ GtkData.AccelMap.load accel_file;
let p = !current in
let m = Config_lexer.load_file pref_file in