diff --git a/configure.in b/configure.in index a540a85790b7ca65e0dcc41e7190f2edc0e7cc46..324d2a99676f5e3e9c14ebbcc0d336f36158a516 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