aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/Makefile.devel
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-04 18:07:16 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-04 18:07:16 +0000
commit43856804207ac43b9ded2609fe7a422db5f62dc4 (patch)
treee517f68ce2c43b719f7480ff8f45a0eec0298d46 /dev/tools/Makefile.devel
parent58c70113a815a42593c566f64f2de840fc7e48a1 (diff)
one more substitution s/Set/Type/
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10617 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/tools/Makefile.devel')
0 files changed, 0 insertions, 0 deletions