diff options
| author | Emilio Jesus Gallego Arias | 2018-11-05 04:03:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-05 18:52:14 +0100 |
| commit | 33cc626936d2c05a98ebf6d2e31bda7217c030b1 (patch) | |
| tree | 9bcd5b1e388938d75f3cb42f8d147234982aa3b7 /dev/tools | |
| parent | efe60d3c1b09bc059053b7383e068ddc05248dac (diff) | |
[dune] Add to vo rules explicit location of coqlib in boot mode.
When `-coqlib $PATH` is absent, Coq will try to locate coqlib using a
heuristic based on the name of the executable.
The code in `envars.ml` basically does:
```ocaml
Filename.(dirname CUnix.(canonical_path_name (dirname Sys.executable_name)))
```
which doesn't seem to work very well on Windows and OSX when `coqtop`
is a symlink.
Instead, we now pass the right `-coqlib` to coqtop from `coq_dune`.
Maybe fixes #8862.
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions
