diff --git a/Makefile b/Makefile index bff43dc18047e29822e5ff19c1e95dbf839fbd92..fbfcdce80f735d1a3daedccb8e986ec0e4778a98 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 12cb8fb3639ecc8dcea9e9775ca426a9c1397ec5..ad8ff1721d19eb805ee9a59883fcc2ee8048ca83 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