From 1dda3ff073193785c68166f33154db36cb270c95 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 10 Oct 2018 19:34:21 +0200
Subject: [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.
---
 tools/coq_dune.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools')

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 *)
-- 
cgit v1.2.3