diff options
| author | Emilio Jesus Gallego Arias | 2018-09-05 20:12:23 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-05 20:46:12 +0200 |
| commit | 340088bbc08d5a3f55110dc2d287a83866ad2740 (patch) | |
| tree | 1b0124815bcd48867557b8a5d046782501666306 /kernel/type_errors.mli | |
| parent | 579f30a53809f9cf73aa3d7c69960b50fc51c7fc (diff) | |
[bin] Fix binary location procedure to work with symlinks.
In #7860 `Sys.executable_name` was introduced to locate coq private
binaries; however, this breaks use cases with symlinks, such as Dune.
In order to fix this, we adopt a simpler strategy; we will always
adapt the name originally provided by the user, and only add a
directory if it was originally present.
This should work (hopefully) in all cases.
This fixes `coqide` not working on Dune builds.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions