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