diff options
| author | Guillaume Melquiond | 2015-04-03 08:48:30 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-04-03 08:48:30 +0200 |
| commit | b667f6fec675d3a05ba0475bdb84beaeed7622ac (patch) | |
| tree | 46923bcb0238d744e66c4acf4dcbb67d40d5b0c3 /ide/ideutils.mli | |
| parent | 6950837dd6e2a3a2bc3c3d748d06054a625bc661 (diff) | |
Use the directory of the current session for selecting files to open.
The old behavior was extremely annoying, especially when using coqide from
the command line, since the "open" box would then point to a seemingly
random point of the filesystem rather than to the directory of the files
currently being edited (since they were passed on the command line rather
than by point-and-click).
The new behavior matches the one of mainstream editors, e.g. emacs, gedit.
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index c2b51dd396..1fb30e4d72 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -29,7 +29,7 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter val find_tag_start : GText.tag -> GText.iter -> GText.iter val find_tag_stop : GText.tag -> GText.iter -> GText.iter -val select_file_for_open : title:string -> unit -> string option +val select_file_for_open : title:string -> ?filename:string -> unit -> string option val select_file_for_save : title:string -> ?filename:string -> unit -> string option val try_convert : string -> string |