From dfdd02518ddff0c4d288377e00e3d9f4f1f89e08 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 26 Jul 2022 15:10:08 +0200
Subject: [PATCH] [dev] adds help message in disable-plugins.sh

---
 dev/disable-plugins.sh | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/dev/disable-plugins.sh b/dev/disable-plugins.sh
index 96ce47d2b42..12cb8fb3639 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
-- 
GitLab