aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorbarras2008-11-13 12:57:53 +0000
committerbarras2008-11-13 12:57:53 +0000
commit6c79471f2d1f358b51ba367b094d4b01486a490c (patch)
tree1a44b4a7384b18ab0cb6403c7c1a149b2866682a /scripts
parent1f645556ceb902d1ce3379411a52329299b4bb5d (diff)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions