diff --git a/dev/disable-plugins.sh b/dev/disable-plugins.sh index 96ce47d2b42971f6e6fc6a21511fe6477d1a2222..12cb8fb3639ecc8dcea9e9775ca426a9c1397ec5 100755 --- a/dev/disable-plugins.sh +++ b/dev/disable-plugins.sh @@ -21,6 +21,14 @@ # # ########################################################################## +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" + exit 0 +esac + if [ ! -f VERSION ]; then echo "This script is meant to be run from the root directory of Frama-C" exit 2 @@ -35,7 +43,12 @@ fi PLUGINS= for PLUGIN in "$@" ; do - PLUGINS="$PLUGINS $PLUGIN" + if [ -d "src/plugins/$PLUGIN" ]; then + PLUGINS="$PLUGINS $PLUGIN" + else + echo "Error: src/plugins/$PLUGIN is not a directory" + exit 2 + fi done cat > src/plugins/dune <<EOL