diff options
| author |  Clément Pit-Claudel <cpitclaudel@users.noreply.github.com> | 2018-10-30 10:36:05 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2018-10-30 10:36:05 -0400 |
| commit | 798739255ec1002438b6f9250acac9786ca28554 (patch) | |
| tree | d056d0ac857e5a32dcdc3cb5d92ef553f3070c7c /coq/coq-compile-common.el | |
| parent | 5b7b84bc5b44fd87905b16a67367ece4e7fa7ee3 (diff) | |
| parent | c32a3ac3de75eb9c94dbfd417a0c6508d350fa69 (diff) | |
Merge pull request #396 from dbp/coqproject-local
Use non-remote path to expand paths in _CoqProject when file is remote.
Diffstat (limited to 'coq/coq-compile-common.el')
0 files changed, 0 insertions, 0 deletions