aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorbarras2010-07-28 13:47:12 +0000
committerbarras2010-07-28 13:47:12 +0000
commit03b782e0cec7c294db4b9cd445bd209e38c1cb0a (patch)
tree02849e81ea61f9a73ce6728625b1772089cd37de /plugins
parent41494147b4b7c9a33721faf8e0041900a8df9d64 (diff)
ported r13340 to trunk
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13341 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions