From 1adaacab1b3e621549fc49cf7b0c665973b88950 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 Jul 2022 14:12:38 +0000
Subject: [PATCH] [dev] (disable-plugins) more precise message for cleaning

---
 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 54d98033e12..f8dd83fbe2d 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
 
-- 
GitLab