diff options
| -rw-r--r-- | ide/preferences.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 57bc0f583f..3893d023bd 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -263,8 +263,6 @@ let get_unicode_bindings_default_file () = (** Hooks *) -(** New style preferences *) - let cmd_coqtop = new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string) @@ -645,8 +643,6 @@ let tag_button () = let box = GPack.hbox () in new tag_button (Gobject.unsafe_cast box#as_widget) -(** Old style preferences *) - let save_pref () = if not (Sys.file_exists (Minilib.coqide_config_home ())) then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; |