From 5e98e848d9c4780b6a994dafc0c19c7ca187034a Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 24 Jun 2022 09:46:46 +0200
Subject: [PATCH] [dune] configure plugin list (cont.)

---
 configure.in | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/configure.in b/configure.in
index a540a85790b..324d2a99676 100644
--- a/configure.in
+++ b/configure.in
@@ -603,8 +603,11 @@ m4_foreach_w([__plugin],m4_esyscmd([ls src/plugins]),
   ])
 
 if test -f src/plugins/.disabled ; then
-  echo "(data_only_dirs $(cat src/plugins/.disabled))" > src/plugins/dune
-  chmod a-w  src/plugins/dune
+  echo ";; File generated by ./configure --disable-<PLUGIN>" > src/plugins/dune
+  echo "(include_subdirs no)" >> src/plugins/dune
+  echo ";; Disabled plugin list:" >> src/plugins/dune
+  echo "(data_only_dirs $(cat src/plugins/.disabled))" >> src/plugins/dune
+  chmod a-w src/plugins/dune
   rm src/plugins/.disabled
 fi
 
-- 
GitLab