diff options
| author | Emilio Jesus Gallego Arias | 2017-12-20 11:11:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-02-14 00:39:17 +0100 |
| commit | d643abd6bc67ed6fb3064316cdca19d5f1564418 (patch) | |
| tree | 285da23f0e442b0f917dab1215934837e1d9d0db /dev/tools | |
| parent | 52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff) | |
[build] Fix VM dynamic linking prep in byte builds.
We correctly set the path of `libcoqrun` in non-local builds. This bug
was introduced by #6038.
c.f. #6475 , #5992.
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions