Suggest to use clean rather than archclean before recompiling.

For instance, generated files depend on whether configuration is done
with dynlink or not and they should be cleaned.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15854 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/configure b/configure
index 1f87c9dd1..874818aae 100755
--- a/configure
+++ b/configure
@@ -1198,5 +1198,5 @@ chmod a-w "$config_file"
 echo "If anything in the above is wrong, please restart './configure'."
 echo
 echo "*Warning* To compile the system for a new architecture"
-echo "          don't forget to do a 'make archclean' before './configure'."
+echo "          don't forget to do a 'make clean' before './configure'."