diff options
Diffstat (limited to 'otherlibs/labltk/browser/editor.ml')
| -rw-r--r-- | otherlibs/labltk/browser/editor.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/otherlibs/labltk/browser/editor.ml b/otherlibs/labltk/browser/editor.ml index ceadef8f7..a8cca85ac 100644 --- a/otherlibs/labltk/browser/editor.ml +++ b/otherlibs/labltk/browser/editor.ml @@ -402,12 +402,14 @@ class editor ~top ~menus = object (self) if txt.name <> name then current_dir <- Filename.dirname name; try if Sys.file_exists name then - if txt.name = name then - Sys.rename name (name ^ "~") - else begin match - Jg_message.ask ~master:top ~title:"Save" - ("File `" ^ name ^ "' exists. Overwrite it?") - with `yes -> () | `no | `cancel -> raise Exit + if txt.name = name then begin + let backup = name ^ "~" in + if Sys.file_exists backup then Sys.remove backup; + try Sys.rename name backup with Sys_error _ -> () + end else begin + match Jg_message.ask ~master:top ~title:"Save" + ("File `" ^ name ^ "' exists. Overwrite it?") + with `yes -> () | `no | `cancel -> raise Exit end; let file = open_out name in let text = Text.get txt.tw ~start:tstart ~stop:(tposend 1) in |