From 1935cb6d6dcb8661772924823f1530c2916bccd0 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 30 Jun 2022 08:00:35 +0200
Subject: [PATCH] [Configure] disabled plugins are listed by 'dune build
 @frama-c-configure'

---
 configure.in | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/configure.in b/configure.in
index 3ad3a3279d1..2962072db6a 100644
--- a/configure.in
+++ b/configure.in
@@ -607,10 +607,11 @@ if test -f src/plugins/.disabled ; then
   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
+  cat src/plugins/.disabled | sed -n -e 's|^\(.*\)$|(rule (alias "frama-c-configure") (deps (universe)) (action (echo "Disabled plug-in: src/plugins/\1\n")))|p' >> src/plugins/dune
   echo ";; Test" >> src/plugins/dune
   echo "(alias (name ptests) (deps (alias ptests_config)))" >> src/plugins/dune
 # "sed -n" is the posix version of "sed --quiet"
-  cat src/plugins/.disabled | sed -n -e 's/^\(.*\)$/(rule (alias "ptests_config") (deps (universe)) (action (echo "Warning: testing with disabled \1 plug-in\n")))/p' >> src/plugins/dune
+  cat src/plugins/.disabled | sed -n -e 's|^\(.*\)$|(rule (alias "ptests_config") (deps (universe)) (action (echo "Testing with disabled plug-in: src/plugins/\1\n")))|p' >> src/plugins/dune
   chmod a-w src/plugins/dune
   rm src/plugins/.disabled
 fi
-- 
GitLab