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 /tools | |
| parent | 4a6ddf4fdc4790fc407dc98bcfb80fd816cab304 (diff) | |
| parent | 1dda3ff073193785c68166f33154db36cb270c95 (diff) | |
Merge PR #8698: [dune] Require that `plugin_base.dune` exists in plugin dirs.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_dune.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index ff6cefdf24..4f4e6d5d6f 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -226,7 +226,8 @@ let scan_mlg4 m d = List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4 let scan_plugins m = - let dirs = Sys.(List.filter (fun f -> is_directory @@ "plugins/"^f) Array.(to_list @@ readdir "plugins/")) in + let is_plugin_directory dir = Sys.(is_directory dir && file_exists (dir ^ "/plugin_base.dune")) in + let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ "plugins/"^f) Array.(to_list @@ readdir "plugins/")) in List.fold_left scan_mlg4 m dirs (* Process .vfiles.d and generate a skeleton for the dune file *) |