From e3f4984c244df6109d0ac41fbe84daae66dbd3ec Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 27 Jul 2022 10:12:30 +0200
Subject: [PATCH] [build] accept also comma-separated plugins list for
DISABLED_PLUGINS
---
dev/disable-plugins.sh | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/dev/disable-plugins.sh b/dev/disable-plugins.sh
index ad8ff1721d1..840a9d3f0cb 100755
--- a/dev/disable-plugins.sh
+++ b/dev/disable-plugins.sh
@@ -41,8 +41,10 @@ if [[ "$#" == "0" || ( "$#" == "1" && "$1" == "none" ) ]]; then
exit 0
fi
+IFS='\, ' read -a DISABLED_PLUGINS <<< "$@"
+
PLUGINS=
-for PLUGIN in "$@" ; do
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
if [ -d "src/plugins/$PLUGIN" ]; then
PLUGINS="$PLUGINS $PLUGIN"
else
@@ -63,7 +65,7 @@ cat > src/plugins/dune <<EOL
(echo "Disabled plug-in(s):\n")
EOL
-for PLUGIN in "$@" ; do
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
echo " (echo \"- src/plugins/$PLUGIN\n\")" >> src/plugins/dune
done
@@ -77,7 +79,7 @@ cat >> src/plugins/dune <<EOL
(action (progn
(echo "Testing with disabled plug-in(s):\n")
EOL
-for PLUGIN in "$@" ; do
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
echo " (echo \"- src/plugins/$PLUGIN\n\")" >> src/plugins/dune
done
echo ")))" >> src/plugins/dune
--
GitLab