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 | |
| 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.
| -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 *) |