aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-08-25 19:05:15 +0000
committerGravatar lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-08-25 19:05:15 +0000
commit430bb930ecaf76d7360969741ce9da619a9f9a89 (patch)
treea3e92a2915878643b0af9c1b2200880360b3bc1b /ide
parentab499065872141132a3afdecbc1182222994d215 (diff)
install-doc* are PHONY
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12292 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions