diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-26 21:51:49 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-26 21:51:49 +0200 |
| commit | 3cf7a09799982924453df29b3bb4d081a0e089b4 (patch) | |
| tree | e544a555d64e35460c034b576690fb36d055fe38 /ide/coqide.ml | |
| parent | 2e3835560ce221f8e4686062502ab24ae63a388d (diff) | |
Open the file chooser even if there is no current session. (Fix bug #4206)
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 0f4cb7b07..c0e228125 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -253,14 +253,14 @@ let newfile _ = !refresh_editor_hook (); notebook#goto_page index -let load sn = - let filename = sn.fileops#filename in +let load _ = + let filename = + try notebook#current_term.fileops#filename + with Invalid_argument _ -> None in match select_file_for_open ~title:"Load file" ?filename () with | None -> () | Some f -> FileAux.load_file f -let load = cb_on_current_term load - let save _ = on_current_term (FileAux.check_save ~saveas:false) let saveas sn = |