From 1df6edee09329311b54a2f4dca904aafc3455948 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 Jul 2022 06:14:56 +0000
Subject: [PATCH] [dev] typo in displable-plugins

---
 dev/disable-plugins.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/disable-plugins.sh b/dev/disable-plugins.sh
index 840a9d3f0cb..54d98033e12 100755
--- a/dev/disable-plugins.sh
+++ b/dev/disable-plugins.sh
@@ -36,7 +36,7 @@ fi
 
 if [[ "$#" == "0" || ( "$#" == "1" && "$1" == "none" ) ]]; then
   rm -f src/plugins/dune
-  echo "All plugin enabled"
+  echo "All plugins enabled"
   echo "Make sure to clean the current directory before rebuilding"
   exit 0
 fi
-- 
GitLab