Skip to content
Snippets Groups Projects
Commit 1adaacab authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[dev] (disable-plugins) more precise message for cleaning

parent 77c8bae3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
dev/disable-plugins.sh
+ 1
− 1
View file @ 1adaacab
...@@ -37,7 +37,7 @@ fi ...@@ -37,7 +37,7 @@ fi
if [[ "$#" == "0" || ( "$#" == "1" && "$1" == "none" ) ]]; then if [[ "$#" == "0" || ( "$#" == "1" && "$1" == "none" ) ]]; then
rm -f src/plugins/dune rm -f src/plugins/dune
echo "All plugins enabled" 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 exit 0
fi fi
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment