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 /dev/base_include | |
| 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 'dev/base_include')
0 files changed, 0 insertions, 0 deletions