aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-11 09:59:09 +0000
committerGravatar lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-11 09:59:09 +0000
commitb0f53dde478905a69982948d69eab2f025c8b14a (patch)
treef1d594e49bd678cb2e3621825435eba0c6113e60 /Makefile
parent1b7b14ab1d0683fc053c635a7db98941bdf89ab9 (diff)
Document how FIND_VCS_CLAUSE has to be used
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11911 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index be3e6054f..033762128 100644
--- a/Makefile
+++ b/Makefile
@@ -24,6 +24,8 @@
# by Emacs' next-error.
###########################################################################
+# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
+# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !!
export FIND_VCS_CLAUSE:='(' \
-name '{arch}' -or \
-name '.svn' -or \