diff options
| -rw-r--r-- | ide/preferences.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 3d7b0017cb..203e81b017 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -184,7 +184,7 @@ let save_pref () = add "encoding_manual" [p.encoding_manual] ++ add "automatic_tactics" - (List.fold_left (fun l v -> v::l) [] p.automatic_tactics) ++ + (List.rev p.automatic_tactics) ++ add "cmd_print" [p.cmd_print] ++ add "modifier_for_navigation" (List.map mod_to_str p.modifier_for_navigation) ++ |