aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/preferences.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-02 18:52:36 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-02 18:52:36 +0000
commit8a72970933994c9670e570fb6f3f768e14143237 (patch)
tree16f65b04b8bcf611dcf7456f95de7937a12c3b30 /ide/preferences.ml
parentc9d0def2241f020070a41551ef9700b8cc345e53 (diff)
Fixed previous commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15272 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r--ide/preferences.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 2303b0011..b976eba3d 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -268,10 +268,9 @@ let save_pref () =
let load_pref () =
let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
- let p = current in
let m = Config_lexer.load_file loaded_pref_file in
- let np = { p with cmd_coqc = p.cmd_coqc } in
+ let np = current in
let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in
let set_hd k f = set k (fun v -> f (List.hd v)) in
let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in