diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index c4c2c0da82..6a4833ec88 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -205,7 +205,9 @@ let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () = file_chooser#add_select_button_stock `SAVE `SAVE ; file_chooser#add_filter (filter_coq_files ()); file_chooser#add_filter (filter_all_files ()); -(* file_chooser#set_do_overwrite_confirmation true;*) + (* this line will be used when a lablgtk >= 2.10.0 is the default on most distributions + file_chooser#set_do_overwrite_confirmation true; + *) ignore (file_chooser#set_current_folder !dir); ignore (file_chooser#set_current_name filename); |