[build] shortcut for disabling plugins before build

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

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