From b667f6fec675d3a05ba0475bdb84beaeed7622ac Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 3 Apr 2015 08:48:30 +0200 Subject: 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. --- ide/ideutils.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide/ideutils.mli') diff --git a/ide/ideutils.mli b/ide/ideutils.mli index c2b51dd39..1fb30e4d7 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 -- cgit v1.2.3