From d1fb79f4469eda2a15c79d14e1c292abb9d45adc Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 4 Oct 2012 22:08:11 +0000 Subject: 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 --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') 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'." -- cgit v1.2.3