diff options
| author |  Daniel Patterson <dbp@dbpmail.net> | 2018-10-29 21:09:00 -0400 |
|---|---|---|
| committer | Daniel Patterson <dbp@dbpmail.net> | 2018-10-30 10:24:00 -0400 |
| commit | c32a3ac3de75eb9c94dbfd417a0c6508d350fa69 (patch) | |
| tree | d056d0ac857e5a32dcdc3cb5d92ef553f3070c7c /doc | |
| parent | 5b7b84bc5b44fd87905b16a67367ece4e7fa7ee3 (diff) | |
Use non-remote path to expand paths in _CoqProject when file is remote.
When editing a remote file, the `coqtop` process will itself be remote, which
means that the paths that are passed to it should be _local_, not remote.
Otherwise, paths like '/ssh:hostname:/path/to/dir' get passed to `coqtop`, which
has no idea what's going on.
This relates to #203.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions