diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 00:32:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-27 16:53:06 +0200 |
| commit | 19f5b6a7d467f75b334e769ebe30cf6459c86855 (patch) | |
| tree | 63c2fe552a85bebae728e13930add7a097159b43 /Makefile.dev | |
| parent | 64a8f3cbb2fa278ed9d7bf2e5567d4e2b9bfa9dc (diff) | |
[configure] Don't die if the build sandbox doesn't have the stdlib.
Dune calls `./configure` under the build sandbox, which, if the voboot
target has not been executed will contain only the OCaml parts of Coq.
Thus, we make configure not to die if the `plugins` directory is not
present.
This makes Dune usable without calling the `voboot` target.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions