diff --git a/dev/disable-plugins.sh b/dev/disable-plugins.sh
index 840a9d3f0cbe268fd7017e045688ca13ce1ea0c1..54d98033e127ce2494ebafd47f77eb8db1a34da8 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