From 397523eaa83a4dfa7ed03d36a52f6921ac1859f6 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 26 Jul 2022 17:22:40 +0200
Subject: [PATCH] [build] shortcut for disabling plugins before build
---
Makefile | 7 +++++++
dev/disable-plugins.sh | 12 ++++++------
2 files changed, 13 insertions(+), 6 deletions(-)
diff --git a/Makefile b/Makefile
index bff43dc1804..fbfcdce80f7 100644
--- a/Makefile
+++ b/Makefile
@@ -62,6 +62,11 @@ FRAMAC_HDRCK_SRC:=tools/hdrck
.PHONY: all
all:
+ifneq ($(DISABLED_PLUGINS),)
+ dune clean
+ rm -rf _build .merlin
+ ./dev/disable-plugins.sh ${DISABLED_PLUGINS}
+endif
dune build $(DUNE_BUILD_OPTS) @install
clean:: purge-tests # to be done before a "dune" command
@@ -78,6 +83,8 @@ help::
@echo "Build configuration variables"
@echo " - RELEASE: compile in release mode if set to 'yes'"
@echo " - DUNE_DISPLAY: parameter transmitted to dune --display option"
+ @echo " - DISABLED_PLUGINS: disable these plugins before (re)building"
+ @echo " (none for enabling all plugins)"
##############################################################################
# INSTALL/UNINSTALL
diff --git a/dev/disable-plugins.sh b/dev/disable-plugins.sh
index 12cb8fb3639..ad8ff1721d1 100755
--- a/dev/disable-plugins.sh
+++ b/dev/disable-plugins.sh
@@ -25,7 +25,7 @@ case "$1" in
"-h"|"--help")
echo "Usage: $0 <plugin directories>"
echo " - directories are given without prefix src/plugins"
- echo " - if no directory is given all plugins are enabled"
+ echo " - if no directory is given all plugins are enabled (alternative: none)"
exit 0
esac
@@ -34,7 +34,7 @@ if [ ! -f VERSION ]; then
exit 2
fi
-if [ $# == "0" ]; then
+if [[ "$#" == "0" || ( "$#" == "1" && "$1" == "none" ) ]]; then
rm -f src/plugins/dune
echo "All plugin enabled"
echo "Make sure to clean the current directory before rebuilding"
@@ -60,11 +60,11 @@ cat > src/plugins/dune <<EOL
(alias "frama-c-configure")
(deps (universe))
(action (progn
- (echo "Disabled plug-in(s):")
+ (echo "Disabled plug-in(s):\n")
EOL
for PLUGIN in "$@" ; do
- echo " (echo \"- src/plugins/$PLUGIN\")" >> src/plugins/dune
+ echo " (echo \"- src/plugins/$PLUGIN\n\")" >> src/plugins/dune
done
cat >> src/plugins/dune <<EOL
@@ -75,10 +75,10 @@ cat >> src/plugins/dune <<EOL
(alias "ptests_config")
(deps (universe))
(action (progn
- (echo "Testing with disabled plug-in(s):")
+ (echo "Testing with disabled plug-in(s):\n")
EOL
for PLUGIN in "$@" ; do
- echo " (echo \"- src/plugins/$PLUGIN\")" >> src/plugins/dune
+ echo " (echo \"- src/plugins/$PLUGIN\n\")" >> src/plugins/dune
done
echo ")))" >> src/plugins/dune
--
GitLab