Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

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

1 files changed, 2 insertions, 2 deletions

diff --git a/Makefile b/Makefile
index 1413d0faa..e8f5fabfe 100644
--- a/Makefile
+++ b/Makefile
@@ -196,8 +196,8 @@ indepclean:
 	rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 	find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f
 	find . -name '*_mod.ml' | xargs rm -f
-	find contrib test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
-	rm -f */*.pp[iox] contrib/*/*.pp[iox]
+	find plugins test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
+	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
 	rm -f toplevel/mltop.byteml toplevel/mltop.optml
 	rm -f test-suite/check.log