diff options
| author | Emilio Jesus Gallego Arias | 2020-03-03 21:28:47 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-03 21:38:42 -0500 |
| commit | 3940ca86e18e6274719d0b435d769ec8a06af7a7 (patch) | |
| tree | 731eaab2e6fc32616e4d8df9a0712f47ead8d37f /dev | |
| parent | 18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (diff) | |
[dune] Fix bug in auto-configure deps.
`plugins` needs to be present to coq_makefile variables are properly
initialized.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions