diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/preferences.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index ed4f4cd1f3..3116be1afc 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -236,9 +236,9 @@ let save_pref () = let () = try GtkData.AccelMap.save accel_file with _ -> () in let p = current in - let add = Util.Stringmap.add in + let add = Util.String.Map.add in let (++) x f = f x in - Util.Stringmap.empty ++ + Util.String.Map.empty ++ add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++ add "cmd_coqc" [p.cmd_coqc] ++ add "cmd_make" [p.cmd_make] ++ @@ -302,7 +302,7 @@ let load_pref () = let m = Config_lexer.load_file loaded_pref_file in let np = current in - let set k f = try let v = Util.Stringmap.find k m in f v with _ -> () in + let set k f = try let v = Util.String.Map.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 let set_int k f = set_hd k (fun v -> f (int_of_string v)) in |