diff options
| author | Théo Zimmermann | 2018-10-11 15:23:42 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-11 15:23:42 +0200 |
| commit | 868d5cd983318bff00292329a3920c3b65eb3ada (patch) | |
| tree | b8c905a0292c5d85a46c2b3926d493877c6d2828 /vernac/comProgramFixpoint.ml | |
| parent | 4a6ddf4fdc4790fc407dc98bcfb80fd816cab304 (diff) | |
| parent | 1dda3ff073193785c68166f33154db36cb270c95 (diff) | |
Merge PR #8698: [dune] Require that `plugin_base.dune` exists in plugin dirs.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions