diff options
| author | Emilio Jesus Gallego Arias | 2018-10-10 19:34:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-10 19:34:21 +0200 |
| commit | 1dda3ff073193785c68166f33154db36cb270c95 (patch) | |
| tree | 018ccb1b211a1ecdc549ddefacc78345c1b1c4f9 /vernac/comProgramFixpoint.ml | |
| parent | 040ad198e38776bb9f398329243b2fe41434f2d5 (diff) | |
[dune] Require that `plugin_base.dune` exists in plugin dirs.
`coq_dune` should not consider a directory as a plugin one if the
`plugin_base.dune` file doesn't exists, as the generated `dune` file
for that dir will try to include it.
We have had problems with this in the past due to spurious dirs.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions